Theorem eleq1 2292

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 2239	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	anbi1d 465	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	exbidv 1871	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		df-clel 2225	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
5		df-clel 2225	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395  ∃wex 1538   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12  2294  eleq1i  2295  eleq1d  2298  eleq1a  2301  cleqh  2329  nelneq  2330  clelsb1  2334  nfcjust  2360  cleqf  2397  nelne2  2491  neleq1  2499  rgen2a  2584  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2798  eqvisset  2811  ceqsralt  2828  vtoclgaf  2867  vtocl2gaf  2869  vtocl3gaf  2871  rspct  2901  rspc  2902  rspce  2903  rspc2gv  2920  ceqsrexv  2934  ceqsrexbv  2935  clel2  2937  elabgt  2945  elabgf  2946  elrabi  2957  elrabf  2958  elrab3t  2959  ralab2  2968  rexab2  2970  mo2icl  2983  morex  2988  reu2  2992  reu6  2993  rmo4  2997  reu8  3000  reuind  3009  nelrdva  3011  ru  3028  dfsbcq  3031  dfsbcq2  3032  sbc8g  3037  sbcel1v  3092  rmob  3123  difjust  3199  unjust  3201  injust  3203  eldif  3207  dfss2f  3216  uniiunlem  3314  elun  3346  elin  3388  rabn0m  3520  disjne  3546  r19.3rm  3581  r19.9rmv  3584  raaanlem  3597  raaan  3598  elif  3615  ifmdc  3646  elpwg  3658  elpr2  3689  elsn2g  3700  rabsn  3734  tpid3g  3785  snssb  3804  snssgOLD  3807  difsn  3808  sssnm  3835  opeq1  3860  opeq2  3861  eluni  3894  elunii  3896  eluniab  3903  elint  3932  elintg  3934  elintab  3937  elintrabg  3939  intss1  3941  eliun  3972  eliin  3973  dfiunv2  4004  opabss  4151  cbvmpt  4182  trel  4192  trss  4194  ssex  4224  intnexr  4239  intexabim  4240  exmidel  4293  euabex  4315  elopab  4350  opelopab2a  4357  frirrg  4445  tz7.2  4449  ordelord  4476  onm  4496  ralxfr2d  4559  rexxfr2d  4560  rabxfrd  4564  reuhypd  4566  ordtriexmid  4617  ontriexmidim  4618  ordtri2orexmid  4619  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  ordsucunielexmid  4627  regexmidlem1  4629  elirr  4637  nordeq  4640  sucprcreg  4645  en2lp  4650  ordsoexmid  4658  ordsuc  4659  onsucuni2  4660  tfis  4679  peano2  4691  findes  4699  limom  4710  opelxp  4753  opeliunxp  4779  opbrop  4803  ssrel  4812  ssrel2  4814  ssrelrel  4824  relopabi  4853  eliunxp  4867  opeliunxp2  4868  ideqg  4879  reldmm  4948  dmmrnm  4949  dmxpm  4950  elreldm  4956  elrnmptg  4982  elres  5047  resiexg  5056  dfres2  5063  imai  5090  elimasng  5102  issref  5117  xpmlem  5155  xpm  5156  elxp4  5222  elxp5  5223  unielrel  5262  relcnvexb  5274  dmfex  5523  funfveu  5648  funimass4  5692  fvelimab  5698  ssimaex  5703  fvopab3g  5715  fvopab3ig  5716  fvmptssdm  5727  chfnrn  5754  fvelrn  5774  fmpt  5793  ffnfv  5801  fmptco  5809  elunirn  5902  f1elima  5909  cbvriota  5978  acexmidlemab  6007  acexmidlemcase  6008  cbvmpox  6094  eloprabga  6103  resoprab  6112  elrnmpo  6130  ov  6136  ovig  6138  ov6g  6155  ovg  6156  ovelrn  6166  caovimo  6211  fo1stresm  6319  fo2ndresm  6320  elxp6  6327  unielxp  6332  eqop2  6336  dfoprab4  6350  dfoprab4f  6351  fmpox  6360  1stconst  6381  2ndconst  6382  f1o2ndf1  6388  xporderlem  6391  f1od2  6395  disjxp1  6396  opeliunxp2f  6399  dftpos3  6423  dftpos4  6424  tpostpos  6425  smoel  6461  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcl  6525  frecabcl  6560  frecsuc  6568  nntri3or  6656  nntri3  6660  nndcel  6663  riinerm  6772  th3qlem1  6801  mapsncnv  6859  elixpsn  6899  dom2lem  6940  fiprc  6985  xpsnen  7000  phplem3g  7037  phpelm  7048  ssfiexmid  7058  domfiexmid  7060  elssdc  7087  inffiexmid  7091  undifdcss  7108  opabfi  7123  snon0  7125  f1dmvrnfibi  7134  f1vrnfibi  7135  ordiso2  7225  ctssdclemn0  7300  ctssdc  7303  enumct  7305  nnnninf  7316  nnnninfeq  7318  nninfisollemne  7321  nninfisol  7323  finomni  7330  exmidlpo  7333  pr2cv1  7391  acneq  7407  finacn  7409  acfun  7412  exmidontriimlem3  7428  exmidontriimlem4  7429  pw1ne1  7437  onntri35  7445  exmidapne  7469  ccfunen  7473  cc2lem  7475  elni2  7524  recexnq  7600  recmulnqg  7601  enq0enq  7641  enq0sym  7642  enq0ref  7643  enq0tr  7644  enq0breq  7646  nqnq0pi  7648  nqnq0  7651  prop  7685  prcdnql  7694  prcunqu  7695  prubl  7696  prltlu  7697  prnmaxl  7698  prnminu  7699  prdisj  7702  prarloc  7713  genipv  7719  genpelvl  7722  genpelvu  7723  genprndl  7731  genprndu  7732  distrlem5prl  7796  distrlem5pru  7797  ltexprlemm  7810  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  aptiprleml  7849  aptiprlemu  7850  archpr  7853  cauappcvgprlemm  7855  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  caucvgprlemm  7878  caucvgprlemladdfu  7887  caucvgprprlemmu  7905  elreal2  8040  ltresr  8049  axcnre  8091  axpre-suploclemres  8111  0re  8169  renepnf  8217  renemnf  8218  ltxrlt  8235  eqlei2  8264  0cnALT  8359  sup3exmid  9127  nn1suc  9152  nnne0  9161  xnn0xr  9460  nn0nepnf  9463  elz  9471  elnn0z  9482  elz2  9541  uzind4s  9814  elnn1uz2  9831  qre  9849  elpqb  9874  xnn0lenn0nn0  10090  xsubge0  10106  xposdif  10107  xleaddadd  10112  fzsn  10291  fz1sbc  10321  elfzp12  10324  fzm1  10325  fz01or  10336  fvinim0ffz  10477  suprzubdc  10486  zsupssdc  10488  xqltnle  10517  flqidz  10536  ceilqidz  10568  modqmuladdnn0  10620  frec2uzrand  10657  frecuzrdgtcl  10664  fzfig  10682  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  iseqf1olemqval  10752  seq3id2  10778  seqhomog  10782  1exp  10820  bcval  11001  hashennn  11032  zfz1isolem1  11094  zfz1iso  11095  seq3coll  11096  iswrdiz  11110  0wrd0  11129  lswlgt0cl  11156  ccatval1  11164  ccatval2  11165  ccatalpha  11180  ccatrcl1  11181  wrdl1s1  11197  ccats1val2  11207  wrd2ind  11294  pfxccatin12lem3  11303  pfxccatid  11312  reuccatpfxs1lem  11317  shftlem  11367  shftfibg  11371  shftfib  11374  shftfn  11375  2shfti  11382  rexuz3  11541  sqrt0rlem  11554  cau3  11666  negfi  11779  sumdc  11909  sumrbdclem  11928  summodclem2a  11932  fisumss  11943  prodrbdclem  12122  prodmodclem2a  12127  fprodssdc  12141  fprodsplit1f  12185  ef0lem  12211  odd2np1  12424  even2n  12425  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  nn0enne  12453  divalgmod  12478  uzwodc  12598  lcmgcdlem  12639  cncongr1  12665  1nprm  12676  isprm2  12679  dvdsnprmd  12687  prmdc  12692  exprmfct  12700  nprmdvds1  12702  coprm  12706  prmdiveq  12798  prm23lt5  12826  pcpre1  12855  pc2dvds  12893  pcz  12895  pcmpt  12906  qexpz  12915  4sqlem2  12952  4sqlem19  12972  ennnfonelemhom  13026  ctiunctlemudc  13048  ssnnctlemct  13057  nninfdclemcl  13059  imasaddfnlemg  13387  ismgmid  13450  isgrpid2  13613  mhmlem  13691  eqgval  13800  dvdsrcl2  14103  nzrunit  14192  lringuplu  14200  dvdsrzring  14607  znrrg  14664  mplsubgfilemm  14702  fiinopn  14718  istopon  14727  basis2  14762  eltg3  14771  tg2  14774  tgidm  14788  bastop  14789  bastop2  14798  topnex  14800  isopn3  14839  tgrest  14883  cnpval  14912  lmbr  14927  cnconst  14948  txbas  14972  uptx  14988  txdis1cn  14992  cnmpt12  15001  cnmpt22  15008  hmeocnvb  15032  xblm  15131  isxms2  15166  mopni  15196  blssioo  15267  dedekindeulemuub  15331  dedekindeulemeu  15336  dedekindicclemuub  15340  dedekindicclemeu  15345  ivthinclemlm  15348  ivthinclemum  15349  ivthreinc  15359  lgsfvalg  15724  lgsval2lem  15729  lgsdir2lem2  15748  gausslemma2dlem1a  15777  gausslemma2dlem4  15783  gausslemma2dlem6  15786  2lgslem1b  15808  2lgs  15823  2lgsoddprmlem2  15825  2lgsoddprmlem3  15830  2sqlem2  15834  2sqlem6  15839  2sqlem7  15840  2sqlem10  15844  vtxvalg  15857  iedgvalg  15858  umgredg  15984  upgrpredgv  15985  usgredg2vlem2  16062  ushgredgedg  16065  ushgredgedgloop  16067  griedg0ssusgr  16090  vtxdgfifival  16097  iswlk  16120  upgrwlkvtxedg  16161  isclwwlknx  16211  clwwlkn1loopb  16215  clwwlknonex2lem1  16232  elabgf0  16309  bj-rspgt  16318  cbvrald  16320  decidi  16327  sumdc2  16331  bdssex  16433  bj-inex  16438  bj-intnexr  16440  bj-unexg  16452  bj-d0clsepcl  16456  bj-nnelirr  16484  bj-nn0suc  16495  bj-inf2vnlem1  16501  bj-inf2vnlem2  16502  bj-inf2vnlem3  16503  bj-inf2vnlem4  16504  bj-nn0sucALT  16509  bj-findis  16510  3dom  16523  trilpolemcl  16577