Theorem eleq1 2175

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 2122	. . . 4 |- ( A = B -> ( x = A <-> x = B ) )
2	1	anbi1d 458	. . 3 |- ( A = B -> ( ( x = A /\ x e. C ) <-> ( x = B /\ x e. C ) ) )
3	2	exbidv 1777	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2109	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2109	. 2 |- ( B e. C <-> E. x ( x = B /\ x e. C ) )
6	3, 4, 5	3bitr4g 222	1 |- ( A = B -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1312   E.wex 1449   e. wcel 1461

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109

This theorem is referenced by:  eleq12  2177  eleq1i  2178  eleq1d  2181  eleq1a  2184  cleqh  2212  nelneq  2213  clelsb3  2217  nfcjust  2241  cleqf  2277  nelne2  2371  neleq1  2379  rgen2a  2458  cbvralf  2620  cbvrexf  2621  cbvreu  2624  cbvrab  2653  eqvisset  2665  ceqsralt  2682  vtoclgaf  2720  vtocl2gaf  2722  vtocl3gaf  2724  rspct  2751  rspc  2752  rspce  2753  rspc2gv  2769  ceqsrexv  2783  ceqsrexbv  2784  clel2  2786  elabgt  2793  elabgf  2794  elrabi  2804  elrabf  2805  elrab3t  2806  ralab2  2815  rexab2  2817  mo2icl  2830  morex  2835  reu2  2839  reu6  2840  rmo4  2844  reu8  2847  reuind  2856  nelrdva  2858  ru  2875  dfsbcq  2878  dfsbcq2  2879  sbc8g  2883  sbcel1v  2937  rmob  2967  difjust  3036  unjust  3038  injust  3040  eldif  3044  dfss2f  3052  uniiunlem  3149  elun  3181  elin  3223  rabn0m  3354  disjne  3380  r19.3rm  3415  r19.9rmv  3418  raaanlem  3432  raaan  3433  ifmdc  3473  elpwg  3482  elpr2  3513  elsn2g  3522  rabsn  3554  tpid3g  3602  snssg  3620  difsn  3621  sssnm  3645  opeq1  3669  opeq2  3670  eluni  3703  elunii  3705  eluniab  3712  elint  3741  elintg  3743  elintab  3746  elintrabg  3748  intss1  3750  eliun  3781  eliin  3782  dfiunv2  3813  opabss  3950  cbvmpt  3981  trel  3991  trss  3993  ssex  4023  intnexr  4034  intexabim  4035  exmidel  4086  euabex  4105  elopab  4138  opelopab2a  4145  frirrg  4230  tz7.2  4234  ordelord  4261  onm  4281  ralxfr2d  4343  rexxfr2d  4344  rabxfrd  4348  reuhypd  4350  ordtriexmid  4395  ordtri2orexmid  4396  ontr2exmid  4398  onsucsssucexmid  4400  onsucelsucexmid  4403  ordsucunielexmid  4404  regexmidlem1  4406  elirr  4414  nordeq  4417  sucprcreg  4422  en2lp  4427  ordsoexmid  4435  ordsuc  4436  onsucuni2  4437  tfis  4455  peano2  4467  findes  4475  limom  4485  opelxp  4527  opeliunxp  4552  opbrop  4576  ssrel  4585  ssrel2  4587  ssrelrel  4597  relopabi  4623  eliunxp  4636  opeliunxp2  4637  ideqg  4648  dmmrnm  4716  dmxpm  4717  elreldm  4723  elrnmptg  4749  elres  4811  resiexg  4820  dfres2  4827  imai  4851  elimasng  4863  issref  4877  xpmlem  4915  xpm  4916  elxp4  4982  elxp5  4983  unielrel  5022  relcnvexb  5034  dmfex  5268  funfveu  5386  funimass4  5424  fvelimab  5429  ssimaex  5434  fvopab3g  5446  fvopab3ig  5447  fvmptssdm  5457  chfnrn  5483  fvelrn  5503  fmpt  5522  ffnfv  5530  fmptco  5538  elunirn  5619  f1elima  5626  cbvriota  5692  acexmidlemab  5720  acexmidlemcase  5721  cbvmpox  5801  eloprabga  5810  resoprab  5819  elrnmpo  5836  ov  5842  ovig  5844  ov6g  5860  ovg  5861  ovelrn  5871  caovimo  5916  fo1stresm  6011  fo2ndresm  6012  elxp6  6019  unielxp  6024  eqop2  6028  dfoprab4  6042  dfoprab4f  6043  fmpox  6050  1stconst  6070  2ndconst  6071  f1o2ndf1  6077  xporderlem  6080  f1od2  6084  disjxp1  6085  opeliunxp2f  6087  dftpos3  6111  dftpos4  6112  tpostpos  6113  smoel  6149  tfr1onlemaccex  6197  tfrcllemaccex  6210  tfrcl  6213  frecabcl  6248  frecsuc  6256  nntri3or  6341  nntri3  6345  nndcel  6348  riinerm  6454  th3qlem1  6483  mapsncnv  6541  elixpsn  6581  dom2lem  6618  fiprc  6661  xpsnen  6666  phplem3g  6701  phpelm  6711  ssfiexmid  6721  domfiexmid  6723  inffiexmid  6751  undifdcss  6762  snon0  6774  f1dmvrnfibi  6782  f1vrnfibi  6783  ordiso2  6870  ctssdclemn0  6945  ctssdc  6948  enumct  6950  finomni  6960  exmidlpo  6963  nnnninf  6971  acfun  7008  elni2  7064  recexnq  7140  recmulnqg  7141  enq0enq  7181  enq0sym  7182  enq0ref  7183  enq0tr  7184  enq0breq  7186  nqnq0pi  7188  nqnq0  7191  prop  7225  prcdnql  7234  prcunqu  7235  prubl  7236  prltlu  7237  prnmaxl  7238  prnminu  7239  prdisj  7242  prarloc  7253  genipv  7259  genpelvl  7262  genpelvu  7263  genprndl  7271  genprndu  7272  distrlem5prl  7336  distrlem5pru  7337  ltexprlemm  7350  ltexprlemdisj  7356  ltexprlemloc  7357  ltexprlemrl  7360  ltexprlemru  7362  aptiprleml  7389  aptiprlemu  7390  archpr  7393  cauappcvgprlemm  7395  cauappcvgprlemladdfu  7404  cauappcvgprlemladdfl  7405  caucvgprlemm  7418  caucvgprlemladdfu  7427  caucvgprprlemmu  7445  elreal2  7559  ltresr  7568  axcnre  7610  0re  7684  renepnf  7731  renemnf  7732  ltxrlt  7748  eqlei2  7775  0cnALT  7869  sup3exmid  8619  nn1suc  8643  nnne0  8652  xnn0xr  8943  nn0nepnf  8946  elz  8954  elnn0z  8965  elz2  9020  uzind4s  9281  elnn1uz2  9297  qre  9313  xnn0lenn0nn0  9535  xsubge0  9551  xposdif  9552  xleaddadd  9557  fzsn  9733  fz1sbc  9763  elfzp12  9766  fzm1  9767  fz01or  9778  fvinim0ffz  9905  flqidz  9946  ceilqidz  9976  modqmuladdnn0  10028  frec2uzrand  10065  frecuzrdgtcl  10072  fzfig  10090  seq3fveq2  10129  seq3shft2  10133  monoord  10136  seq3split  10139  iseqf1olemqval  10147  seq3id2  10169  1exp  10209  bcval  10382  hashennn  10413  zfz1isolem1  10470  zfz1iso  10471  seq3coll  10472  shftlem  10475  shftfibg  10479  shftfib  10482  shftfn  10483  2shfti  10490  rexuz3  10648  sqrt0rlem  10661  cau3  10773  negfi  10885  sumdc  11013  sumrbdclem  11031  summodclem2a  11036  fisumss  11047  ef0lem  11211  odd2np1  11412  even2n  11413  oddnn02np1  11419  oddge22np1  11420  evennn02n  11421  evennn2n  11422  nn0enne  11441  divalgmod  11466  lcmgcdlem  11598  cncongr1  11624  1nprm  11635  isprm2  11638  dvdsnprmd  11646  exprmfct  11658  nprmdvds1  11660  coprm  11662  ennnfonelemhom  11767  ctiunctlemudc  11787  fiinopn  12008  istopon  12017  basis2  12052  eltg3  12063  tg2  12066  tgidm  12080  bastop  12081  bastop2  12090  topnex  12092  isopn3  12131  tgrest  12175  cnpval  12203  lmbr  12218  cnconst  12239  txbas  12263  uptx  12279  txdis1cn  12283  cnmpt12  12292  cnmpt22  12299  xblm  12400  isxms2  12435  mopni  12465  blssioo  12525  elabgf0  12667  bj-rspgt  12676  cbvrald  12678  decidi  12685  sumdc2  12689  bdssex  12783  bj-inex  12788  bj-intnexr  12790  bj-unexg  12802  bj-d0clsepcl  12806  bj-nnelirr  12834  bj-nn0suc  12845  bj-inf2vnlem1  12851  bj-inf2vnlem2  12852  bj-inf2vnlem3  12853  bj-inf2vnlem4  12854  bj-nn0sucALT  12859  bj-findis  12860  nninfalllemn  12883  trilpolemcl  12911