![]() |
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 2291 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | |
2 | abbii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpgbi 1452 | 1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1353 {cab 2163 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 |
This theorem is referenced by: rabswap 2655 rabbiia 2722 rabab 2758 csb2 3059 cbvcsbw 3061 cbvcsb 3062 csbid 3065 csbco 3067 csbcow 3068 cbvreucsf 3121 unrab 3406 inrab 3407 inrab2 3408 difrab 3409 rabun2 3414 dfnul3 3425 rab0 3451 tprot 3685 pw0 3739 dfuni2 3811 unipr 3823 dfint2 3846 int0 3858 dfiunv2 3922 cbviun 3923 cbviin 3924 iunrab 3934 iunid 3942 viin 3946 cbvopab 4074 cbvopab1 4076 cbvopab2 4077 cbvopab1s 4078 cbvopab2v 4080 unopab 4082 iunopab 4281 abnex 4447 uniuni 4451 ruv 4549 rabxp 4663 dfdm3 4814 dfrn2 4815 dfrn3 4816 dfdm4 4819 dfdmf 4820 dmun 4834 dmopab 4838 dmopabss 4839 dmopab3 4840 dfrnf 4868 rnopab 4874 rnmpt 4875 dfima2 4972 dfima3 4973 imadmrn 4980 imai 4984 args 4997 mptpreima 5122 dfiota2 5179 cbviota 5183 sb8iota 5185 dffv4g 5512 dfimafn2 5565 fnasrn 5694 fnasrng 5696 elabrex 5758 abrexco 5759 dfoprab2 5921 cbvoprab2 5947 dmoprab 5955 rnoprab 5957 rnoprab2 5958 fnrnov 6019 abrexex2g 6120 abrexex2 6124 abexssex 6125 abexex 6126 oprabrexex2 6130 dfopab2 6189 cnvoprab 6234 tfr1onlemaccex 6348 tfrcllemaccex 6361 tfrcldm 6363 frec0g 6397 frecsuc 6407 snec 6595 pmex 6652 dfixp 6699 cbvixp 6714 caucvgprprlemmu 7693 caucvgsr 7800 pitonnlem1 7843 mertenslem2 11539 toponsspwpwg 13413 tgval2 13444 if0ab 14439 bdcuni 14510 bj-dfom 14567 |
Copyright terms: Public domain | W3C validator |