Theorem eleq1 2252

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 2199	. . . 4 |- ( A = B -> ( x = A <-> x = B ) )
2	1	anbi1d 465	. . 3 |- ( A = B -> ( ( x = A /\ x e. C ) <-> ( x = B /\ x e. C ) ) )
3	2	exbidv 1836	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2185	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2185	. 2 |- ( B e. C <-> E. x ( x = B /\ x e. C ) )
6	3, 4, 5	3bitr4g 223	1 |- ( A = B -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   E.wex 1503   e. wcel 2160

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  eleq12  2254  eleq1i  2255  eleq1d  2258  eleq1a  2261  cleqh  2289  nelneq  2290  clelsb1  2294  nfcjust  2320  cleqf  2357  nelne2  2451  neleq1  2459  rgen2a  2544  cbvralf  2710  cbvrexf  2711  cbvreu  2716  cbvrab  2750  eqvisset  2762  ceqsralt  2779  vtoclgaf  2817  vtocl2gaf  2819  vtocl3gaf  2821  rspct  2849  rspc  2850  rspce  2851  rspc2gv  2868  ceqsrexv  2882  ceqsrexbv  2883  clel2  2885  elabgt  2893  elabgf  2894  elrabi  2905  elrabf  2906  elrab3t  2907  ralab2  2916  rexab2  2918  mo2icl  2931  morex  2936  reu2  2940  reu6  2941  rmo4  2945  reu8  2948  reuind  2957  nelrdva  2959  ru  2976  dfsbcq  2979  dfsbcq2  2980  sbc8g  2985  sbcel1v  3040  rmob  3070  difjust  3145  unjust  3147  injust  3149  eldif  3153  dfss2f  3161  uniiunlem  3259  elun  3291  elin  3333  rabn0m  3465  disjne  3491  r19.3rm  3526  r19.9rmv  3529  raaanlem  3543  raaan  3544  ifmdc  3589  elpwg  3598  elpr2  3629  elsn2g  3640  rabsn  3674  tpid3g  3722  snssb  3740  snssgOLD  3743  difsn  3744  sssnm  3769  opeq1  3793  opeq2  3794  eluni  3827  elunii  3829  eluniab  3836  elint  3865  elintg  3867  elintab  3870  elintrabg  3872  intss1  3874  eliun  3905  eliin  3906  dfiunv2  3937  opabss  4082  cbvmpt  4113  trel  4123  trss  4125  ssex  4155  intnexr  4169  intexabim  4170  exmidel  4223  euabex  4243  elopab  4276  opelopab2a  4283  frirrg  4368  tz7.2  4372  ordelord  4399  onm  4419  ralxfr2d  4482  rexxfr2d  4483  rabxfrd  4487  reuhypd  4489  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  ontr2exmid  4542  onsucsssucexmid  4544  onsucelsucexmid  4547  ordsucunielexmid  4548  regexmidlem1  4550  elirr  4558  nordeq  4561  sucprcreg  4566  en2lp  4571  ordsoexmid  4579  ordsuc  4580  onsucuni2  4581  tfis  4600  peano2  4612  findes  4620  limom  4631  opelxp  4674  opeliunxp  4699  opbrop  4723  ssrel  4732  ssrel2  4734  ssrelrel  4744  relopabi  4770  eliunxp  4784  opeliunxp2  4785  ideqg  4796  dmmrnm  4864  dmxpm  4865  elreldm  4871  elrnmptg  4897  elres  4961  resiexg  4970  dfres2  4977  imai  5002  elimasng  5014  issref  5029  xpmlem  5067  xpm  5068  elxp4  5134  elxp5  5135  unielrel  5174  relcnvexb  5186  dmfex  5424  funfveu  5547  funimass4  5587  fvelimab  5593  ssimaex  5598  fvopab3g  5610  fvopab3ig  5611  fvmptssdm  5621  chfnrn  5648  fvelrn  5668  fmpt  5687  ffnfv  5695  fmptco  5703  elunirn  5788  f1elima  5795  cbvriota  5863  acexmidlemab  5891  acexmidlemcase  5892  cbvmpox  5975  eloprabga  5984  resoprab  5993  elrnmpo  6011  ov  6017  ovig  6019  ov6g  6035  ovg  6036  ovelrn  6046  caovimo  6091  fo1stresm  6187  fo2ndresm  6188  elxp6  6195  unielxp  6200  eqop2  6204  dfoprab4  6218  dfoprab4f  6219  fmpox  6226  1stconst  6247  2ndconst  6248  f1o2ndf1  6254  xporderlem  6257  f1od2  6261  disjxp1  6262  opeliunxp2f  6264  dftpos3  6288  dftpos4  6289  tpostpos  6290  smoel  6326  tfr1onlemaccex  6374  tfrcllemaccex  6387  tfrcl  6390  frecabcl  6425  frecsuc  6433  nntri3or  6519  nntri3  6523  nndcel  6526  riinerm  6635  th3qlem1  6664  mapsncnv  6722  elixpsn  6762  dom2lem  6799  fiprc  6842  xpsnen  6848  phplem3g  6885  phpelm  6895  ssfiexmid  6905  domfiexmid  6907  inffiexmid  6935  undifdcss  6952  snon0  6966  f1dmvrnfibi  6974  f1vrnfibi  6975  ordiso2  7065  ctssdclemn0  7140  ctssdc  7143  enumct  7145  nnnninf  7155  nnnninfeq  7157  nninfisollemne  7160  nninfisol  7162  finomni  7169  exmidlpo  7172  acfun  7237  exmidontriimlem3  7253  exmidontriimlem4  7254  pw1ne1  7259  onntri35  7267  exmidapne  7290  ccfunen  7294  cc2lem  7296  elni2  7344  recexnq  7420  recmulnqg  7421  enq0enq  7461  enq0sym  7462  enq0ref  7463  enq0tr  7464  enq0breq  7466  nqnq0pi  7468  nqnq0  7471  prop  7505  prcdnql  7514  prcunqu  7515  prubl  7516  prltlu  7517  prnmaxl  7518  prnminu  7519  prdisj  7522  prarloc  7533  genipv  7539  genpelvl  7542  genpelvu  7543  genprndl  7551  genprndu  7552  distrlem5prl  7616  distrlem5pru  7617  ltexprlemm  7630  ltexprlemdisj  7636  ltexprlemloc  7637  ltexprlemrl  7640  ltexprlemru  7642  aptiprleml  7669  aptiprlemu  7670  archpr  7673  cauappcvgprlemm  7675  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  caucvgprlemm  7698  caucvgprlemladdfu  7707  caucvgprprlemmu  7725  elreal2  7860  ltresr  7869  axcnre  7911  axpre-suploclemres  7931  0re  7988  renepnf  8036  renemnf  8037  ltxrlt  8054  eqlei2  8083  0cnALT  8178  sup3exmid  8945  nn1suc  8969  nnne0  8978  xnn0xr  9275  nn0nepnf  9278  elz  9286  elnn0z  9297  elz2  9355  uzind4s  9622  elnn1uz2  9639  qre  9657  elpqb  9681  xnn0lenn0nn0  9897  xsubge0  9913  xposdif  9914  xleaddadd  9919  fzsn  10098  fz1sbc  10128  elfzp12  10131  fzm1  10132  fz01or  10143  fvinim0ffz  10273  xqltnle  10300  flqidz  10319  ceilqidz  10349  modqmuladdnn0  10401  frec2uzrand  10438  frecuzrdgtcl  10445  fzfig  10463  seq3fveq2  10502  seq3shft2  10506  monoord  10509  seq3split  10512  iseqf1olemqval  10520  seq3id2  10542  1exp  10583  bcval  10764  hashennn  10795  zfz1isolem1  10855  zfz1iso  10856  seq3coll  10857  shftlem  10860  shftfibg  10864  shftfib  10867  shftfn  10868  2shfti  10875  rexuz3  11034  sqrt0rlem  11047  cau3  11159  negfi  11271  sumdc  11401  sumrbdclem  11420  summodclem2a  11424  fisumss  11435  prodrbdclem  11614  prodmodclem2a  11619  fprodssdc  11633  fprodsplit1f  11677  ef0lem  11703  odd2np1  11913  even2n  11914  oddnn02np1  11920  oddge22np1  11921  evennn02n  11922  evennn2n  11923  nn0enne  11942  divalgmod  11967  suprzubdc  11988  zsupssdc  11990  uzwodc  12073  lcmgcdlem  12112  cncongr1  12138  1nprm  12149  isprm2  12152  dvdsnprmd  12160  prmdc  12165  exprmfct  12173  nprmdvds1  12175  coprm  12179  prmdiveq  12271  prm23lt5  12298  pcpre1  12327  pc2dvds  12365  pcz  12367  pcmpt  12378  qexpz  12387  4sqlem2  12424  4sqlem19  12444  ennnfonelemhom  12469  ctiunctlemudc  12491  ssnnctlemct  12500  nninfdclemcl  12502  imasaddfnlemg  12794  ismgmid  12856  isgrpid2  12999  mhmlem  13071  eqgval  13179  dvdsrcl2  13466  nzrunit  13552  lringuplu  13560  dvdsrzring  13919  fiinopn  13981  istopon  13990  basis2  14025  eltg3  14034  tg2  14037  tgidm  14051  bastop  14052  bastop2  14061  topnex  14063  isopn3  14102  tgrest  14146  cnpval  14175  lmbr  14190  cnconst  14211  txbas  14235  uptx  14251  txdis1cn  14255  cnmpt12  14264  cnmpt22  14271  hmeocnvb  14295  xblm  14394  isxms2  14429  mopni  14459  blssioo  14522  dedekindeulemuub  14572  dedekindeulemeu  14577  dedekindicclemuub  14581  dedekindicclemeu  14586  ivthinclemlm  14589  ivthinclemum  14590  lgsfvalg  14884  lgsval2lem  14889  lgsdir2lem2  14908  2lgsoddprmlem2  14932  2lgsoddprmlem3  14937  2sqlem2  14940  2sqlem6  14945  2sqlem7  14946  2sqlem10  14950  elabgf0  15007  bj-rspgt  15016  cbvrald  15018  decidi  15025  sumdc2  15029  bdssex  15132  bj-inex  15137  bj-intnexr  15139  bj-unexg  15151  bj-d0clsepcl  15155  bj-nnelirr  15183  bj-nn0suc  15194  bj-inf2vnlem1  15200  bj-inf2vnlem2  15201  bj-inf2vnlem3  15202  bj-inf2vnlem4  15203  bj-nn0sucALT  15208  bj-findis  15209  trilpolemcl  15264