![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > abbii | GIF version |
Description: Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abbii.1 | ⊢ (φ ↔ ψ) |
Ref | Expression |
---|---|
abbii | ⊢ {x ∣ φ} = {x ∣ ψ} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbi 2148 | . 2 ⊢ (∀x(φ ↔ ψ) ↔ {x ∣ φ} = {x ∣ ψ}) | |
2 | abbii.1 | . 2 ⊢ (φ ↔ ψ) | |
3 | 1, 2 | mpgbi 1338 | 1 ⊢ {x ∣ φ} = {x ∣ ψ} |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 = wceq 1242 {cab 2023 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-11 1394 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 |
This theorem is referenced by: rabswap 2482 rabbiia 2541 rabab 2569 csb2 2848 cbvcsb 2850 csbid 2853 csbco 2855 cbvreucsf 2904 unrab 3202 inrab 3203 inrab2 3204 difrab 3205 rabun2 3210 dfnul3 3221 rab0 3240 tprot 3454 pw0 3502 dfuni2 3573 unipr 3585 dfint2 3608 int0 3620 dfiunv2 3684 cbviun 3685 cbviin 3686 iunrab 3695 iunid 3703 viin 3707 cbvopab 3819 cbvopab1 3821 cbvopab2 3822 cbvopab1s 3823 cbvopab2v 3825 unopab 3827 iunopab 4009 uniuni 4149 ruv 4228 rabxp 4323 dfdm3 4465 dfrn2 4466 dfrn3 4467 dfdm4 4470 dfdmf 4471 dmun 4485 dmopab 4489 dmopabss 4490 dmopab3 4491 dfrnf 4518 rnopab 4524 rnmpt 4525 dfima2 4613 dfima3 4614 imadmrn 4621 imai 4624 args 4637 mptpreima 4757 dfiota2 4811 cbviota 4815 sb8iota 4817 dffv4g 5118 dfimafn2 5166 fnasrn 5284 fnasrng 5286 elabrex 5340 abrexco 5341 dfoprab2 5494 cbvoprab2 5519 dmoprab 5527 rnoprab 5529 rnoprab2 5530 fnrnov 5588 abrexex2g 5689 abrexex2 5693 abexssex 5694 abexex 5695 oprabrexex2 5699 dfopab2 5757 frec0g 5922 frecsuc 5930 snec 6103 pitonnlem1 6741 bdcuni 9331 bj-dfom 9392 |
Copyright terms: Public domain | W3C validator |