Theorem eleq1 2413

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eleq1	⊢ (A = B → (A ∈ C ↔ B ∈ C))

Proof of Theorem eleq1

Dummy variable x is distinct from all other variables.

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))

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