New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eleq1 | GIF version |
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eleq1 | ⊢ (A = B → (A ∈ C ↔ B ∈ C)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2362 | . . . 4 ⊢ (A = B → (x = A ↔ x = B)) | |
2 | 1 | anbi1d 685 | . . 3 ⊢ (A = B → ((x = A ∧ x ∈ C) ↔ (x = B ∧ x ∈ C))) |
3 | 2 | exbidv 1626 | . 2 ⊢ (A = B → (∃x(x = A ∧ x ∈ C) ↔ ∃x(x = B ∧ x ∈ C))) |
4 | df-clel 2349 | . 2 ⊢ (A ∈ C ↔ ∃x(x = A ∧ x ∈ C)) | |
5 | df-clel 2349 | . 2 ⊢ (B ∈ C ↔ ∃x(x = B ∧ x ∈ C)) | |
6 | 3, 4, 5 | 3bitr4g 279 | 1 ⊢ (A = B → (A ∈ C ↔ B ∈ C)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 ∧ wa 358 ∃wex 1541 = wceq 1642 ∈ wcel 1710 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-cleq 2346 df-clel 2349 |
This theorem is referenced by: eleq12 2415 eleq1i 2416 eleq1d 2419 eleq1a 2422 cleqh 2450 nelneq 2451 clelsb3 2455 nfcjust 2477 cleqf 2513 nelne2 2606 neleq1 2607 rgen2a 2680 ralcom2 2775 nfrab 2792 cbvralf 2829 cbvreu 2833 cbvrab 2857 ceqsralt 2882 vtoclgaf 2919 vtocl2gaf 2921 vtocl3gaf 2923 rspct 2948 rspc 2949 rspce 2950 ceqsrexv 2972 ceqsrexbv 2973 clel2 2975 elabgt 2982 elabgf 2983 elrabf 2993 ralab2 3001 rexab2 3003 moeq3 3013 mo2icl 3015 morex 3020 reu2 3024 reu6 3025 rmo4 3029 reu8 3032 reuind 3039 2reu5 3044 ru 3045 dfsbcq 3048 dfsbcq2 3049 sbc8g 3053 sbc2or 3054 sbcel1gv 3105 rmob 3134 ninjust 3210 elning 3217 dfss2f 3264 uniiunlem 3353 disjne 3596 ifel 3697 ifcl 3698 elimel 3714 keepel 3719 elpwg 3729 elpr2 3752 elsnc2g 3761 rabsn 3790 tpid3g 3831 snssg 3844 difsn 3845 sssn 3864 eluni 3894 elunii 3896 eluniab 3903 elint 3932 elintg 3934 elintab 3937 elintrabg 3939 intss1 3941 uniintsn 3963 eliun 3973 eliin 3974 pwadjoin 4119 el1c 4139 elpw1 4144 pw10 4161 eqpw1 4162 pw1in 4164 pw1disj 4167 pw111 4170 eluni1g 4172 elxpk 4196 opkabssvvk 4208 ssrelk 4211 eqrelk 4212 opkelxpkg 4247 cokrelk 4284 sikexlem 4295 dfpw12 4301 insklem 4304 abexv 4324 eqpw1uni 4330 reiota2 4368 nnc0suc 4412 nnsucelrlem2 4425 nnsucelr 4428 nndisjeq 4429 snfi 4431 ltfinex 4464 lenltfin 4469 ssfin 4470 ncfineq 4473 ncfinlower 4483 tfinltfinlem1 4500 evenoddnnnul 4514 nnadjoinpw 4521 sfineq1 4526 sfineq2 4527 sfindbl 4530 sfinltfin 4535 spfinsfincl 4539 vfinspsslem1 4550 vfinspss 4551 vfinspeqtncv 4553 nulnnn 4556 peano4 4557 addccan2 4559 phi11lem1 4595 phi011lem1 4598 phialllem1 4616 opeq 4619 elopab 4696 opelopab2a 4702 setconslem4 4734 setconslem6 4736 brsi 4761 epelc 4765 opeliunxp 4820 eliunxp 4821 opeliunxp2 4822 opbrop 4841 br1st 4858 br2nd 4859 brswap2 4860 ideqg2 4869 elres 4995 dfres2 5002 imai 5010 dfcnv2 5100 elxp4 5108 xpexr 5109 dmfex 5247 dffn5 5363 fvelrnb 5365 funimass4 5368 fvelimab 5370 fvun1 5379 fvopab4t 5385 fvopab3g 5386 fvopab3ig 5387 chfnrn 5399 fnasrn 5417 ffnfv 5427 f1elima 5474 opbr1st 5501 opbr2nd 5502 brswap 5509 xpnedisj 5513 eloprabga 5578 resoprab 5581 ov 5595 ovig 5597 ov6g 5600 ovg 5601 ovelrn 5608 oprssdm 5612 caovmo 5645 cbvmpt 5676 cbvmpt2x 5678 fmpt 5692 ovmpt2x 5712 fmpt2x 5730 elfix 5787 elfunsg 5830 clos1conn 5879 clos1basesuc 5882 dfnnc3 5885 frds 5935 fundmen 6043 enadjlem1 6059 enadj 6060 enprmaplem1 6076 enprmaplem5 6080 elncs 6119 eqnc2 6129 nnnc 6146 ncssfin 6151 ncspw1eu 6159 eqtc 6161 nntccl 6170 ceclb 6183 ce0ncpw1 6185 cecl 6186 nclecid 6197 le0nc 6200 addlecncs 6209 letc 6231 nclenn 6249 ncvsq 6256 nmembers1lem1 6268 nmembers1lem3 6270 spaccl 6286 spacind 6287 nchoicelem3 6291 nchoicelem16 6304 frecxp 6314 dmfrec 6316 fnfreclem3 6319 scancan 6331 |
Copyright terms: Public domain | W3C validator |