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 form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
abbii | ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbi 2231 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | |
2 | abbii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpgbi 1413 | 1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1316 {cab 2103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 |
This theorem is referenced by: rabswap 2586 rabbiia 2645 rabab 2681 csb2 2977 cbvcsb 2979 csbid 2982 csbco 2984 cbvreucsf 3034 unrab 3317 inrab 3318 inrab2 3319 difrab 3320 rabun2 3325 dfnul3 3336 rab0 3361 tprot 3586 pw0 3637 dfuni2 3708 unipr 3720 dfint2 3743 int0 3755 dfiunv2 3819 cbviun 3820 cbviin 3821 iunrab 3830 iunid 3838 viin 3842 cbvopab 3969 cbvopab1 3971 cbvopab2 3972 cbvopab1s 3973 cbvopab2v 3975 unopab 3977 iunopab 4173 abnex 4338 uniuni 4342 ruv 4435 rabxp 4546 dfdm3 4696 dfrn2 4697 dfrn3 4698 dfdm4 4701 dfdmf 4702 dmun 4716 dmopab 4720 dmopabss 4721 dmopab3 4722 dfrnf 4750 rnopab 4756 rnmpt 4757 dfima2 4853 dfima3 4854 imadmrn 4861 imai 4865 args 4878 mptpreima 5002 dfiota2 5059 cbviota 5063 sb8iota 5065 dffv4g 5386 dfimafn2 5439 fnasrn 5566 fnasrng 5568 elabrex 5627 abrexco 5628 dfoprab2 5786 cbvoprab2 5812 dmoprab 5820 rnoprab 5822 rnoprab2 5823 fnrnov 5884 abrexex2g 5986 abrexex2 5990 abexssex 5991 abexex 5992 oprabrexex2 5996 dfopab2 6055 cnvoprab 6099 tfr1onlemaccex 6213 tfrcllemaccex 6226 tfrcldm 6228 frec0g 6262 frecsuc 6272 snec 6458 pmex 6515 dfixp 6562 cbvixp 6577 caucvgprprlemmu 7471 caucvgsr 7578 pitonnlem1 7621 mertenslem2 11260 toponsspwpwg 12100 tgval2 12131 bdcuni 12970 bj-dfom 13027 |
Copyright terms: Public domain | W3C validator |