Theorem eleq1 2147

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 2094	. . . 4 |- ( A = B -> ( x = A <-> x = B ) )
2	1	anbi1d 453	. . 3 |- ( A = B -> ( ( x = A /\ x e. C ) <-> ( x = B /\ x e. C ) ) )
3	2	exbidv 1750	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2081	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2081	. 2 |- ( B e. C <-> E. x ( x = B /\ x e. C ) )
6	3, 4, 5	3bitr4g 221	1 |- ( A = B -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1287   E.wex 1424   e. wcel 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081

This theorem is referenced by:  eleq12  2149  eleq1i  2150  eleq1d  2153  eleq1a  2156  cleqh  2184  nelneq  2185  clelsb3  2189  nfcjust  2213  cleqf  2248  nelne2  2342  neleq1  2350  rgen2a  2425  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvrab  2613  eqvisset  2623  ceqsralt  2640  vtoclgaf  2677  vtocl2gaf  2679  vtocl3gaf  2681  rspct  2708  rspc  2709  rspce  2710  rspc2gv  2725  ceqsrexv  2738  ceqsrexbv  2739  clel2  2741  elabgt  2748  elabgf  2749  elrabi  2759  elrabf  2760  elrab3t  2761  ralab2  2770  rexab2  2772  mo2icl  2785  morex  2790  reu2  2794  reu6  2795  rmo4  2799  reu8  2802  reuind  2809  nelrdva  2811  ru  2828  dfsbcq  2831  dfsbcq2  2832  sbc8g  2836  sbcel1v  2890  rmob  2920  difjust  2989  unjust  2991  injust  2993  eldif  2997  dfss2f  3005  uniiunlem  3098  elun  3130  elin  3172  rabn0m  3299  disjne  3324  r19.3rm  3357  r19.9rmv  3360  raaanlem  3374  raaan  3375  elpwg  3422  elpr2  3452  elsn2g  3459  rabsn  3491  tpid3g  3537  snssg  3555  difsn  3556  sssnm  3580  opeq1  3604  opeq2  3605  eluni  3638  elunii  3640  eluniab  3647  elint  3676  elintg  3678  elintab  3681  elintrabg  3683  intss1  3685  eliun  3716  eliin  3717  dfiunv2  3748  opabss  3876  cbvmpt  3906  trel  3916  trss  3918  ssex  3949  intnexr  3960  intexabim  3961  iinexgm  3963  exmidel  4006  euabex  4024  elopab  4057  opelopab2a  4064  frirrg  4149  tz7.2  4153  ordelord  4180  onm  4200  ralxfr2d  4258  rexxfr2d  4259  rabxfrd  4263  reuhypd  4265  ordtriexmid  4309  ordtri2orexmid  4310  ontr2exmid  4312  onsucsssucexmid  4314  onsucelsucexmid  4317  ordsucunielexmid  4318  regexmidlem1  4320  elirr  4328  nordeq  4331  sucprcreg  4336  en2lp  4341  ordsoexmid  4349  ordsuc  4350  onsucuni2  4351  tfis  4369  peano2  4381  findes  4389  limom  4399  opelxp  4438  opeliunxp  4459  opbrop  4483  ssrel  4492  ssrel2  4494  ssrelrel  4504  relopabi  4529  xpiindim  4539  eliunxp  4541  opeliunxp2  4542  ideqg  4553  dmmrnm  4621  dmxpm  4622  elreldm  4627  elrnmptg  4653  elres  4713  resiexg  4722  dfres2  4727  imai  4751  elimasng  4763  issref  4777  xpmlem  4814  xpm  4815  elxp4  4880  elxp5  4881  unielrel  4920  relcnvexb  4932  cnviinm  4934  dmfex  5156  funfveu  5274  funimass4  5311  fvelimab  5316  ssimaex  5321  fvopab3g  5333  fvopab3ig  5334  fvmptssdm  5343  chfnrn  5366  fvelrn  5386  fmpt  5405  ffnfv  5412  fmptco  5420  elunirn  5499  f1elima  5506  cbvriota  5572  acexmidlemab  5600  acexmidlemcase  5601  cbvmpt2x  5676  eloprabga  5685  resoprab  5691  elrnmpt2  5708  ov  5714  ovig  5716  ov6g  5732  ovg  5733  ovelrn  5743  caovimo  5788  fo1stresm  5882  fo2ndresm  5883  elxp6  5890  unielxp  5894  eqop2  5898  dfoprab4  5912  dfoprab4f  5913  fmpt2x  5920  1stconst  5936  2ndconst  5937  f1o2ndf1  5943  xporderlem  5946  f1od2  5950  dftpos3  5974  dftpos4  5975  tpostpos  5976  smoel  6012  tfr1onlemaccex  6060  tfrcllemaccex  6073  tfrcl  6076  frecabcl  6111  frecsuc  6119  nntri3or  6201  nntri3  6205  nndcel  6208  iinerm  6309  riinerm  6310  th3qlem1  6339  mapsncnv  6397  dom2lem  6434  fiprc  6477  xpsnen  6482  phplem3g  6517  phpelm  6527  ssfiexmid  6537  domfiexmid  6539  inffiexmid  6567  undifdcss  6578  snon0  6588  f1dmvrnfibi  6596  f1vrnfibi  6597  ordiso2  6664  djuun  6696  finomni  6732  nnnninf  6742  elni2  6809  recexnq  6885  recmulnqg  6886  enq0enq  6926  enq0sym  6927  enq0ref  6928  enq0tr  6929  enq0breq  6931  nqnq0pi  6933  nqnq0  6936  prop  6970  prcdnql  6979  prcunqu  6980  prubl  6981  prltlu  6982  prnmaxl  6983  prnminu  6984  prdisj  6987  prarloc  6998  genipv  7004  genpelvl  7007  genpelvu  7008  genprndl  7016  genprndu  7017  distrlem5prl  7081  distrlem5pru  7082  ltexprlemm  7095  ltexprlemdisj  7101  ltexprlemloc  7102  ltexprlemrl  7105  ltexprlemru  7107  aptiprleml  7134  aptiprlemu  7135  archpr  7138  cauappcvgprlemm  7140  cauappcvgprlemladdfu  7149  cauappcvgprlemladdfl  7150  caucvgprlemm  7163  caucvgprlemladdfu  7172  caucvgprprlemmu  7190  elreal2  7304  ltresr  7312  axcnre  7352  0re  7424  renepnf  7471  renemnf  7472  ltxrlt  7488  eqlei2  7515  0cnALT  7608  nn1suc  8368  nnne0  8377  xnn0xr  8666  nn0nepnf  8669  elz  8677  elnn0z  8688  elz2  8743  uzind4s  9002  elnn1uz2  9018  qre  9034  fzsn  9403  fz1sbc  9432  elfzp12  9435  fzm1  9436  fz01or  9447  fvinim0ffz  9572  flqidz  9613  ceilqidz  9643  modqmuladdnn0  9695  frec2uzrand  9732  frecuzrdgtcl  9739  fzfig  9757  iseqfveq2  9794  iseqshft2  9798  monoord  9801  iseqsplit  9804  iseqf1olemqval  9812  iseqid2  9835  1exp  9874  bcval  10045  hashennn  10076  zfz1isolem1  10133  zfz1iso  10134  iseqcoll  10135  shftlem  10138  shftfibg  10142  shftfib  10145  shftfn  10146  2shfti  10153  rexuz3  10310  sqrt0rlem  10323  cau3  10435  negfi  10544  sumdc  10629  isumrblem  10647  isummolem2a  10652  odd2np1  10739  even2n  10740  oddnn02np1  10746  oddge22np1  10747  evennn02n  10748  evennn2n  10749  nn0enne  10768  divalgmod  10793  lcmgcdlem  10925  cncongr1  10951  1nprm  10962  isprm2  10965  dvdsnprmd  10973  exprmfct  10985  nprmdvds1  10987  coprm  10989  elabgf0  11106  bj-rspgt  11115  cbvrald  11117  decidi  11124  sumdc2  11128  bdssex  11222  bj-inex  11227  bj-intnexr  11229  bj-unexg  11241  bj-d0clsepcl  11249  bj-nnelirr  11277  bj-nn0suc  11288  bj-inf2vnlem1  11294  bj-inf2vnlem2  11295  bj-inf2vnlem3  11296  bj-inf2vnlem4  11297  bj-nn0sucALT  11302  bj-findis  11303  nninfalllemn  11327