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 1398  ∃wex 1541   ∈ 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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  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  2363  cleqf  2400  nelne2  2494  neleq1  2502  rgen2a  2587  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvrab  2801  eqvisset  2814  ceqsralt  2831  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  rspct  2904  rspc  2905  rspce  2906  rspc2gv  2923  ceqsrexv  2937  ceqsrexbv  2938  clel2  2940  elabgt  2948  elabgf  2949  elrabi  2960  elrabf  2961  elrab3t  2962  ralab2  2971  rexab2  2973  mo2icl  2986  morex  2991  reu2  2995  reu6  2996  rmo4  3000  reu8  3003  reuind  3012  nelrdva  3014  ru  3031  dfsbcq  3034  dfsbcq2  3035  sbc8g  3040  sbcel1v  3095  rmob  3126  difjust  3202  unjust  3204  injust  3206  eldif  3210  dfss2f  3219  uniiunlem  3318  elun  3350  elin  3392  rabn0m  3524  disjne  3550  r19.3rm  3585  r19.9rmv  3588  raaanlem  3601  raaan  3602  elif  3621  ifmdc  3652  elpwg  3664  elpr2  3695  elsn2g  3706  rabsn  3740  tpid3g  3791  snssb  3811  snssgOLD  3814  difsn  3815  sssnm  3842  opeq1  3867  opeq2  3868  eluni  3901  elunii  3903  eluniab  3910  elint  3939  elintg  3941  elintab  3944  elintrabg  3946  intss1  3948  eliun  3979  eliin  3980  dfiunv2  4011  opabss  4158  cbvmpt  4189  trel  4199  trss  4201  ssex  4231  intnexr  4246  intexabim  4247  exmidel  4301  euabex  4323  elopab  4358  opelopab2a  4365  frirrg  4453  tz7.2  4457  ordelord  4484  onm  4504  ralxfr2d  4567  rexxfr2d  4568  rabxfrd  4572  reuhypd  4574  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  ordsucunielexmid  4635  regexmidlem1  4637  elirr  4645  nordeq  4648  sucprcreg  4653  en2lp  4658  ordsoexmid  4666  ordsuc  4667  onsucuni2  4668  tfis  4687  peano2  4699  findes  4707  limom  4718  opelxp  4761  opeliunxp  4787  opbrop  4811  ssrel  4820  ssrel2  4822  ssrelrel  4832  relopabi  4861  eliunxp  4875  opeliunxp2  4876  ideqg  4887  reldmm  4956  dmmrnm  4957  dmxpm  4958  elreldm  4964  elrnmptg  4990  elres  5055  resiexg  5064  dfres2  5071  imai  5099  elimasng  5111  issref  5126  xpmlem  5164  xpm  5165  elxp4  5231  elxp5  5232  unielrel  5271  relcnvexb  5283  dmfex  5535  funfveu  5661  funimass4  5705  fvelimab  5711  ssimaex  5716  fvopab3g  5728  fvopab3ig  5729  fvmptssdm  5740  chfnrn  5767  fvelrn  5786  fmpt  5805  ffnfv  5813  fmptco  5821  elunirn  5917  f1elima  5924  cbvriota  5993  acexmidlemab  6022  acexmidlemcase  6023  cbvmpox  6109  eloprabga  6118  resoprab  6127  elrnmpo  6145  ov  6151  ovig  6153  ov6g  6170  ovg  6171  ovelrn  6181  caovimo  6226  fo1stresm  6333  fo2ndresm  6334  elxp6  6341  unielxp  6346  eqop2  6350  dfoprab4  6364  dfoprab4f  6365  fmpox  6374  1stconst  6395  2ndconst  6396  f1o2ndf1  6402  xporderlem  6405  f1od2  6409  disjxp1  6410  opeliunxp2f  6447  dftpos3  6471  dftpos4  6472  tpostpos  6473  smoel  6509  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcl  6573  frecabcl  6608  frecsuc  6616  nntri3or  6704  nntri3  6708  nndcel  6711  riinerm  6820  th3qlem1  6849  mapsncnv  6907  elixpsn  6947  dom2lem  6988  fiprc  7033  xpsnen  7048  phplem3g  7085  phpelm  7096  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  elssdc  7137  inffiexmid  7141  undifdcss  7158  opabfi  7175  snon0  7177  f1dmvrnfibi  7186  f1vrnfibi  7187  ordiso2  7277  ctssdclemn0  7352  ctssdc  7355  enumct  7357  nnnninf  7368  nnnninfeq  7370  nninfisollemne  7373  nninfisol  7375  finomni  7382  exmidlpo  7385  pr2cv1  7443  acneq  7460  finacn  7462  acfun  7465  exmidontriimlem3  7481  exmidontriimlem4  7482  pw1ne1  7490  onntri35  7498  exmidapne  7522  ccfunen  7526  cc2lem  7528  elni2  7577  recexnq  7653  recmulnqg  7654  enq0enq  7694  enq0sym  7695  enq0ref  7696  enq0tr  7697  enq0breq  7699  nqnq0pi  7701  nqnq0  7704  prop  7738  prcdnql  7747  prcunqu  7748  prubl  7749  prltlu  7750  prnmaxl  7751  prnminu  7752  prdisj  7755  prarloc  7766  genipv  7772  genpelvl  7775  genpelvu  7776  genprndl  7784  genprndu  7785  distrlem5prl  7849  distrlem5pru  7850  ltexprlemm  7863  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  aptiprleml  7902  aptiprlemu  7903  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  caucvgprlemm  7931  caucvgprlemladdfu  7940  caucvgprprlemmu  7958  elreal2  8093  ltresr  8102  axcnre  8144  axpre-suploclemres  8164  0re  8222  renepnf  8269  renemnf  8270  ltxrlt  8287  eqlei2  8316  0cnALT  8411  sup3exmid  9179  nn1suc  9204  nnne0  9213  xnn0xr  9514  nn0nepnf  9517  elz  9525  elnn0z  9536  elz2  9595  uzind4s  9868  elnn1uz2  9885  qre  9903  elpqb  9928  xnn0lenn0nn0  10144  xsubge0  10160  xposdif  10161  xleaddadd  10166  fzsn  10346  fz1sbc  10376  elfzp12  10379  fzm1  10380  fz01or  10391  fvinim0ffz  10533  suprzubdc  10542  zsupssdc  10544  xqltnle  10573  flqidz  10592  ceilqidz  10624  modqmuladdnn0  10676  frec2uzrand  10713  frecuzrdgtcl  10720  fzfig  10738  seq3fveq2  10783  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  monoord  10793  seq3split  10796  seqsplitg  10797  iseqf1olemqval  10808  seq3id2  10834  seqhomog  10838  1exp  10876  bcval  11057  hashennn  11088  zfz1isolem1  11150  zfz1iso  11151  seq3coll  11152  iswrdiz  11169  0wrd0  11188  lswlgt0cl  11215  ccatval1  11223  ccatval2  11224  ccatalpha  11239  ccatrcl1  11240  wrdl1s1  11256  ccats1val2  11266  wrd2ind  11353  pfxccatin12lem3  11362  pfxccatid  11371  reuccatpfxs1lem  11376  shftlem  11439  shftfibg  11443  shftfib  11446  shftfn  11447  2shfti  11454  rexuz3  11613  sqrt0rlem  11626  cau3  11738  negfi  11851  sumdc  11981  sumrbdclem  12001  summodclem2a  12005  fisumss  12016  prodrbdclem  12195  prodmodclem2a  12200  fprodssdc  12214  fprodsplit1f  12258  ef0lem  12284  odd2np1  12497  even2n  12498  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  nn0enne  12526  divalgmod  12551  uzwodc  12671  lcmgcdlem  12712  cncongr1  12738  1nprm  12749  isprm2  12752  dvdsnprmd  12760  prmdc  12765  exprmfct  12773  nprmdvds1  12775  coprm  12779  prmdiveq  12871  prm23lt5  12899  pcpre1  12928  pc2dvds  12966  pcz  12968  pcmpt  12979  qexpz  12988  4sqlem2  13025  4sqlem19  13045  ennnfonelemhom  13099  ctiunctlemudc  13121  ssnnctlemct  13130  nninfdclemcl  13132  imasaddfnlemg  13460  ismgmid  13523  isgrpid2  13686  mhmlem  13764  eqgval  13873  dvdsrcl2  14177  nzrunit  14266  lringuplu  14274  dvdsrzring  14682  znrrg  14739  mplsubgfilemm  14782  fiinopn  14798  istopon  14807  basis2  14842  eltg3  14851  tg2  14854  tgidm  14868  bastop  14869  bastop2  14878  topnex  14880  isopn3  14919  tgrest  14963  cnpval  14992  lmbr  15007  cnconst  15028  txbas  15052  uptx  15068  txdis1cn  15072  cnmpt12  15081  cnmpt22  15088  hmeocnvb  15112  xblm  15211  isxms2  15246  mopni  15276  blssioo  15347  dedekindeulemuub  15411  dedekindeulemeu  15416  dedekindicclemuub  15420  dedekindicclemeu  15425  ivthinclemlm  15428  ivthinclemum  15429  ivthreinc  15439  pellexlem3  15776  lgsfvalg  15807  lgsval2lem  15812  lgsdir2lem2  15831  gausslemma2dlem1a  15860  gausslemma2dlem4  15866  gausslemma2dlem6  15869  2lgslem1b  15891  2lgs  15906  2lgsoddprmlem2  15908  2lgsoddprmlem3  15913  2sqlem2  15917  2sqlem6  15922  2sqlem7  15923  2sqlem10  15927  vtxvalg  15940  iedgvalg  15941  umgredg  16069  upgrpredgv  16070  usgredg2vlem2  16147  ushgredgedg  16150  ushgredgedgloop  16152  griedg0ssusgr  16175  uhgrspansubgrlem  16200  vtxdgfifival  16215  iswlk  16247  upgrwlkvtxedg  16288  isclwwlknx  16340  clwwlkn1loopb  16344  clwwlknonex2lem1  16361  elabgf0  16478  bj-rspgt  16487  cbvrald  16489  decidi  16496  sumdc2  16500  bdssex  16601  bj-inex  16606  bj-intnexr  16608  bj-unexg  16620  bj-d0clsepcl  16624  bj-nnelirr  16652  bj-nn0suc  16663  bj-inf2vnlem1  16669  bj-inf2vnlem2  16670  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672  bj-nn0sucALT  16677  bj-findis  16678  3dom  16691  trilpolemcl  16752