Theorem eleq1 2294

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

Assertion

Ref	Expression
eleq1	⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Proof of Theorem eleq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2241	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	anbi1d 465	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	exbidv 1873	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		df-clel 2227	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
5		df-clel 2227	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1397  ∃wex 1540   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12  2296  eleq1i  2297  eleq1d  2300  eleq1a  2303  cleqh  2331  nelneq  2332  clelsb1  2336  nfcjust  2362  cleqf  2399  nelne2  2493  neleq1  2501  rgen2a  2586  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvrab  2800  eqvisset  2813  ceqsralt  2830  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  rspce  2905  rspc2gv  2922  ceqsrexv  2936  ceqsrexbv  2937  clel2  2939  elabgt  2947  elabgf  2948  elrabi  2959  elrabf  2960  elrab3t  2961  ralab2  2970  rexab2  2972  mo2icl  2985  morex  2990  reu2  2994  reu6  2995  rmo4  2999  reu8  3002  reuind  3011  nelrdva  3013  ru  3030  dfsbcq  3033  dfsbcq2  3034  sbc8g  3039  sbcel1v  3094  rmob  3125  difjust  3201  unjust  3203  injust  3205  eldif  3209  dfss2f  3218  uniiunlem  3316  elun  3348  elin  3390  rabn0m  3522  disjne  3548  r19.3rm  3583  r19.9rmv  3586  raaanlem  3599  raaan  3600  elif  3617  ifmdc  3648  elpwg  3660  elpr2  3691  elsn2g  3702  rabsn  3736  tpid3g  3787  snssb  3806  snssgOLD  3809  difsn  3810  sssnm  3837  opeq1  3862  opeq2  3863  eluni  3896  elunii  3898  eluniab  3905  elint  3934  elintg  3936  elintab  3939  elintrabg  3941  intss1  3943  eliun  3974  eliin  3975  dfiunv2  4006  opabss  4153  cbvmpt  4184  trel  4194  trss  4196  ssex  4226  intnexr  4241  intexabim  4242  exmidel  4295  euabex  4317  elopab  4352  opelopab2a  4359  frirrg  4447  tz7.2  4451  ordelord  4478  onm  4498  ralxfr2d  4561  rexxfr2d  4562  rabxfrd  4566  reuhypd  4568  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  elirr  4639  nordeq  4642  sucprcreg  4647  en2lp  4652  ordsoexmid  4660  ordsuc  4661  onsucuni2  4662  tfis  4681  peano2  4693  findes  4701  limom  4712  opelxp  4755  opeliunxp  4781  opbrop  4805  ssrel  4814  ssrel2  4816  ssrelrel  4826  relopabi  4855  eliunxp  4869  opeliunxp2  4870  ideqg  4881  reldmm  4950  dmmrnm  4951  dmxpm  4952  elreldm  4958  elrnmptg  4984  elres  5049  resiexg  5058  dfres2  5065  imai  5092  elimasng  5104  issref  5119  xpmlem  5157  xpm  5158  elxp4  5224  elxp5  5225  unielrel  5264  relcnvexb  5276  dmfex  5526  funfveu  5652  funimass4  5696  fvelimab  5702  ssimaex  5707  fvopab3g  5719  fvopab3ig  5720  fvmptssdm  5731  chfnrn  5758  fvelrn  5778  fmpt  5797  ffnfv  5805  fmptco  5813  elunirn  5907  f1elima  5914  cbvriota  5983  acexmidlemab  6012  acexmidlemcase  6013  cbvmpox  6099  eloprabga  6108  resoprab  6117  elrnmpo  6135  ov  6141  ovig  6143  ov6g  6160  ovg  6161  ovelrn  6171  caovimo  6216  fo1stresm  6324  fo2ndresm  6325  elxp6  6332  unielxp  6337  eqop2  6341  dfoprab4  6355  dfoprab4f  6356  fmpox  6365  1stconst  6386  2ndconst  6387  f1o2ndf1  6393  xporderlem  6396  f1od2  6400  disjxp1  6401  opeliunxp2f  6404  dftpos3  6428  dftpos4  6429  tpostpos  6430  smoel  6466  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcl  6530  frecabcl  6565  frecsuc  6573  nntri3or  6661  nntri3  6665  nndcel  6668  riinerm  6777  th3qlem1  6806  mapsncnv  6864  elixpsn  6904  dom2lem  6945  fiprc  6990  xpsnen  7005  phplem3g  7042  phpelm  7053  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  elssdc  7094  inffiexmid  7098  undifdcss  7115  opabfi  7132  snon0  7134  f1dmvrnfibi  7143  f1vrnfibi  7144  ordiso2  7234  ctssdclemn0  7309  ctssdc  7312  enumct  7314  nnnninf  7325  nnnninfeq  7327  nninfisollemne  7330  nninfisol  7332  finomni  7339  exmidlpo  7342  pr2cv1  7400  acneq  7417  finacn  7419  acfun  7422  exmidontriimlem3  7438  exmidontriimlem4  7439  pw1ne1  7447  onntri35  7455  exmidapne  7479  ccfunen  7483  cc2lem  7485  elni2  7534  recexnq  7610  recmulnqg  7611  enq0enq  7651  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  nqnq0pi  7658  nqnq0  7661  prop  7695  prcdnql  7704  prcunqu  7705  prubl  7706  prltlu  7707  prnmaxl  7708  prnminu  7709  prdisj  7712  prarloc  7723  genipv  7729  genpelvl  7732  genpelvu  7733  genprndl  7741  genprndu  7742  distrlem5prl  7806  distrlem5pru  7807  ltexprlemm  7820  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  aptiprleml  7859  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemm  7888  caucvgprlemladdfu  7897  caucvgprprlemmu  7915  elreal2  8050  ltresr  8059  axcnre  8101  axpre-suploclemres  8121  0re  8179  renepnf  8227  renemnf  8228  ltxrlt  8245  eqlei2  8274  0cnALT  8369  sup3exmid  9137  nn1suc  9162  nnne0  9171  xnn0xr  9470  nn0nepnf  9473  elz  9481  elnn0z  9492  elz2  9551  uzind4s  9824  elnn1uz2  9841  qre  9859  elpqb  9884  xnn0lenn0nn0  10100  xsubge0  10116  xposdif  10117  xleaddadd  10122  fzsn  10301  fz1sbc  10331  elfzp12  10334  fzm1  10335  fz01or  10346  fvinim0ffz  10488  suprzubdc  10497  zsupssdc  10499  xqltnle  10528  flqidz  10547  ceilqidz  10579  modqmuladdnn0  10631  frec2uzrand  10668  frecuzrdgtcl  10675  fzfig  10693  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  iseqf1olemqval  10763  seq3id2  10789  seqhomog  10793  1exp  10831  bcval  11012  hashennn  11043  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  iswrdiz  11124  0wrd0  11143  lswlgt0cl  11170  ccatval1  11178  ccatval2  11179  ccatalpha  11194  ccatrcl1  11195  wrdl1s1  11211  ccats1val2  11221  wrd2ind  11308  pfxccatin12lem3  11317  pfxccatid  11326  reuccatpfxs1lem  11331  shftlem  11381  shftfibg  11385  shftfib  11388  shftfn  11389  2shfti  11396  rexuz3  11555  sqrt0rlem  11568  cau3  11680  negfi  11793  sumdc  11923  sumrbdclem  11943  summodclem2a  11947  fisumss  11958  prodrbdclem  12137  prodmodclem2a  12142  fprodssdc  12156  fprodsplit1f  12200  ef0lem  12226  odd2np1  12439  even2n  12440  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  nn0enne  12468  divalgmod  12493  uzwodc  12613  lcmgcdlem  12654  cncongr1  12680  1nprm  12691  isprm2  12694  dvdsnprmd  12702  prmdc  12707  exprmfct  12715  nprmdvds1  12717  coprm  12721  prmdiveq  12813  prm23lt5  12841  pcpre1  12870  pc2dvds  12908  pcz  12910  pcmpt  12921  qexpz  12930  4sqlem2  12967  4sqlem19  12987  ennnfonelemhom  13041  ctiunctlemudc  13063  ssnnctlemct  13072  nninfdclemcl  13074  imasaddfnlemg  13402  ismgmid  13465  isgrpid2  13628  mhmlem  13706  eqgval  13815  dvdsrcl2  14119  nzrunit  14208  lringuplu  14216  dvdsrzring  14623  znrrg  14680  mplsubgfilemm  14718  fiinopn  14734  istopon  14743  basis2  14778  eltg3  14787  tg2  14790  tgidm  14804  bastop  14805  bastop2  14814  topnex  14816  isopn3  14855  tgrest  14899  cnpval  14928  lmbr  14943  cnconst  14964  txbas  14988  uptx  15004  txdis1cn  15008  cnmpt12  15017  cnmpt22  15024  hmeocnvb  15048  xblm  15147  isxms2  15182  mopni  15212  blssioo  15283  dedekindeulemuub  15347  dedekindeulemeu  15352  dedekindicclemuub  15356  dedekindicclemeu  15361  ivthinclemlm  15364  ivthinclemum  15365  ivthreinc  15375  lgsfvalg  15740  lgsval2lem  15745  lgsdir2lem2  15764  gausslemma2dlem1a  15793  gausslemma2dlem4  15799  gausslemma2dlem6  15802  2lgslem1b  15824  2lgs  15839  2lgsoddprmlem2  15841  2lgsoddprmlem3  15846  2sqlem2  15850  2sqlem6  15855  2sqlem7  15856  2sqlem10  15860  vtxvalg  15873  iedgvalg  15874  umgredg  16002  upgrpredgv  16003  usgredg2vlem2  16080  ushgredgedg  16083  ushgredgedgloop  16085  griedg0ssusgr  16108  uhgrspansubgrlem  16133  vtxdgfifival  16148  iswlk  16180  upgrwlkvtxedg  16221  isclwwlknx  16273  clwwlkn1loopb  16277  clwwlknonex2lem1  16294  elabgf0  16399  bj-rspgt  16408  cbvrald  16410  decidi  16417  sumdc2  16421  bdssex  16523  bj-inex  16528  bj-intnexr  16530  bj-unexg  16542  bj-d0clsepcl  16546  bj-nnelirr  16574  bj-nn0suc  16585  bj-inf2vnlem1  16591  bj-inf2vnlem2  16592  bj-inf2vnlem3  16593  bj-inf2vnlem4  16594  bj-nn0sucALT  16599  bj-findis  16600  3dom  16613  trilpolemcl  16667