Theorem eleq1 2413

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

Assertion

Ref	Expression
eleq1	|- (A = B -> (A e. C <-> B e. 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 e. C) <-> (x = B /\ x e. C)))
3	2	exbidv 1626	. 2 |- (A = B -> (E.x(x = A /\ x e. C) <-> E.x(x = B /\ x e. C)))
4		df-clel 2349	. 2 |- (A e. C <-> E.x(x = A /\ x e. C))
5		df-clel 2349	. 2 |- (B e. C <-> E.x(x = B /\ x e. C))
6	3, 4, 5	3bitr4g 279	1 |- (A = B -> (A e. C <-> B e. C))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  E.wex 1541   = wceq 1642   e. 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  clelsb1  2455  nfcjust  2478  cleqf  2514  nelne2  2607  neleq1  2608  rgen2a  2681  ralcom2  2776  nfrab  2793  cbvralf  2830  cbvreu  2834  cbvrab  2858  ceqsralt  2883  vtoclgaf  2920  vtocl2gaf  2922  vtocl3gaf  2924  rspct  2949  rspc  2950  rspce  2951  ceqsrexv  2973  ceqsrexbv  2974  clel2  2976  elabgt  2983  elabgf  2984  elrabf  2994  ralab2  3002  rexab2  3004  moeq3  3014  mo2icl  3016  morex  3021  reu2  3025  reu6  3026  rmo4  3030  reu8  3033  reuind  3040  2reu5  3045  ru  3046  dfsbcq  3049  dfsbcq2  3050  sbc8g  3054  sbc2or  3055  sbcel1gv  3106  rmob  3135  ninjust  3211  elning  3218  dfss2f  3265  uniiunlem  3354  disjne  3597  ifel  3698  ifcl  3699  elimel  3715  keepel  3720  elpwg  3730  elpr2  3753  elsnc2g  3762  rabsn  3791  tpid3g  3832  snssg  3845  difsn  3846  sssn  3865  eluni  3895  elunii  3897  eluniab  3904  elint  3933  elintg  3935  elintab  3938  elintrabg  3940  intss1  3942  uniintsn  3964  eliun  3974  eliin  3975  pwadjoin  4120  el1c  4140  elpw1  4145  pw10  4162  eqpw1  4163  pw1in  4165  pw1disj  4168  pw111  4171  eluni1g  4173  elxpk  4197  opkabssvvk  4209  ssrelk  4212  eqrelk  4213  opkelxpkg  4248  cokrelk  4285  sikexlem  4296  dfpw12  4302  insklem  4305  abexv  4325  eqpw1uni  4331  reiota2  4369  nnc0suc  4413  nnsucelrlem2  4426  nnsucelr  4429  nndisjeq  4430  snfi  4432  ltfinex  4465  lenltfin  4470  ssfin  4471  ncfineq  4474  ncfinlower  4484  tfinltfinlem1  4501  evenoddnnnul  4515  nnadjoinpw  4522  sfineq1  4527  sfineq2  4528  sfindbl  4531  sfinltfin  4536  spfinsfincl  4540  vfinspsslem1  4551  vfinspss  4552  vfinspeqtncv  4554  nulnnn  4557  peano4  4558  addccan2  4560  phi11lem1  4596  phi011lem1  4599  phialllem1  4617  opeq  4620  elopab  4697  opelopab2a  4703  setconslem4  4735  setconslem6  4737  brsi  4762  epelc  4766  opeliunxp  4821  eliunxp  4822  opeliunxp2  4823  opbrop  4842  br1st  4859  br2nd  4860  brswap2  4861  ideqg2  4870  elres  4996  dfres2  5003  imai  5011  dfcnv2  5101  elxp4  5109  xpexr  5110  dmfex  5248  dffn5  5364  fvelrnb  5366  funimass4  5369  fvelimab  5371  fvun1  5380  fvopab4t  5386  fvopab3g  5387  fvopab3ig  5388  chfnrn  5400  fnasrn  5418  ffnfv  5428  f1elima  5475  opbr1st  5502  opbr2nd  5503  brswap  5510  xpnedisj  5514  eloprabga  5579  resoprab  5582  ov  5596  ovig  5598  ov6g  5601  ovg  5602  ovelrn  5609  oprssdm  5613  caovmo  5646  cbvmpt  5677  cbvmpt2x  5679  fmpt  5693  ovmpt2x  5713  fmpt2x  5731  elfix  5788  elfunsg  5831  clos1conn  5880  clos1basesuc  5883  dfnnc3  5886  frds  5936  fundmen  6044  enadjlem1  6060  enadj  6061  enprmaplem1  6077  enprmaplem5  6081  elncs  6120  eqnc2  6130  nnnc  6147  ncssfin  6152  ncspw1eu  6160  eqtc  6162  nntccl  6171  ceclb  6184  ce0ncpw1  6186  cecl  6187  nclecid  6198  le0nc  6201  addlecncs  6210  letc  6232  nclenn  6250  ncvsq  6257  nmembers1lem1  6269  nmembers1lem3  6271  spaccl  6287  spacind  6288  nchoicelem3  6292  nchoicelem16  6305  frecxp  6315  dmfrec  6317  fnfreclem3  6320  scancan  6332