Theorem eleq1 2240

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353  ∃wex 1492   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12  2242  eleq1i  2243  eleq1d  2246  eleq1a  2249  cleqh  2277  nelneq  2278  clelsb1  2282  nfcjust  2307  cleqf  2344  nelne2  2438  neleq1  2446  rgen2a  2531  cbvralf  2697  cbvrexf  2698  cbvreu  2702  cbvrab  2736  eqvisset  2748  ceqsralt  2765  vtoclgaf  2803  vtocl2gaf  2805  vtocl3gaf  2807  rspct  2835  rspc  2836  rspce  2837  rspc2gv  2854  ceqsrexv  2868  ceqsrexbv  2869  clel2  2871  elabgt  2879  elabgf  2880  elrabi  2891  elrabf  2892  elrab3t  2893  ralab2  2902  rexab2  2904  mo2icl  2917  morex  2922  reu2  2926  reu6  2927  rmo4  2931  reu8  2934  reuind  2943  nelrdva  2945  ru  2962  dfsbcq  2965  dfsbcq2  2966  sbc8g  2971  sbcel1v  3026  rmob  3056  difjust  3131  unjust  3133  injust  3135  eldif  3139  dfss2f  3147  uniiunlem  3245  elun  3277  elin  3319  rabn0m  3451  disjne  3477  r19.3rm  3512  r19.9rmv  3515  raaanlem  3529  raaan  3530  ifmdc  3575  elpwg  3584  elpr2  3615  elsn2g  3626  rabsn  3660  tpid3g  3708  snssb  3726  snssgOLD  3729  difsn  3730  sssnm  3755  opeq1  3779  opeq2  3780  eluni  3813  elunii  3815  eluniab  3822  elint  3851  elintg  3853  elintab  3856  elintrabg  3858  intss1  3860  eliun  3891  eliin  3892  dfiunv2  3923  opabss  4068  cbvmpt  4099  trel  4109  trss  4111  ssex  4141  intnexr  4152  intexabim  4153  exmidel  4206  euabex  4226  elopab  4259  opelopab2a  4266  frirrg  4351  tz7.2  4355  ordelord  4382  onm  4402  ralxfr2d  4465  rexxfr2d  4466  rabxfrd  4470  reuhypd  4472  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  onsucelsucexmid  4530  ordsucunielexmid  4531  regexmidlem1  4533  elirr  4541  nordeq  4544  sucprcreg  4549  en2lp  4554  ordsoexmid  4562  ordsuc  4563  onsucuni2  4564  tfis  4583  peano2  4595  findes  4603  limom  4614  opelxp  4657  opeliunxp  4682  opbrop  4706  ssrel  4715  ssrel2  4717  ssrelrel  4727  relopabi  4753  eliunxp  4767  opeliunxp2  4768  ideqg  4779  dmmrnm  4847  dmxpm  4848  elreldm  4854  elrnmptg  4880  elres  4944  resiexg  4953  dfres2  4960  imai  4985  elimasng  4997  issref  5012  xpmlem  5050  xpm  5051  elxp4  5117  elxp5  5118  unielrel  5157  relcnvexb  5169  dmfex  5406  funfveu  5529  funimass4  5567  fvelimab  5573  ssimaex  5578  fvopab3g  5590  fvopab3ig  5591  fvmptssdm  5601  chfnrn  5628  fvelrn  5648  fmpt  5667  ffnfv  5675  fmptco  5683  elunirn  5767  f1elima  5774  cbvriota  5841  acexmidlemab  5869  acexmidlemcase  5870  cbvmpox  5953  eloprabga  5962  resoprab  5971  elrnmpo  5988  ov  5994  ovig  5996  ov6g  6012  ovg  6013  ovelrn  6023  caovimo  6068  fo1stresm  6162  fo2ndresm  6163  elxp6  6170  unielxp  6175  eqop2  6179  dfoprab4  6193  dfoprab4f  6194  fmpox  6201  1stconst  6222  2ndconst  6223  f1o2ndf1  6229  xporderlem  6232  f1od2  6236  disjxp1  6237  opeliunxp2f  6239  dftpos3  6263  dftpos4  6264  tpostpos  6265  smoel  6301  tfr1onlemaccex  6349  tfrcllemaccex  6362  tfrcl  6365  frecabcl  6400  frecsuc  6408  nntri3or  6494  nntri3  6498  nndcel  6501  riinerm  6608  th3qlem1  6637  mapsncnv  6695  elixpsn  6735  dom2lem  6772  fiprc  6815  xpsnen  6821  phplem3g  6856  phpelm  6866  ssfiexmid  6876  domfiexmid  6878  inffiexmid  6906  undifdcss  6922  snon0  6935  f1dmvrnfibi  6943  f1vrnfibi  6944  ordiso2  7034  ctssdclemn0  7109  ctssdc  7112  enumct  7114  nnnninf  7124  nnnninfeq  7126  nninfisollemne  7129  nninfisol  7131  finomni  7138  exmidlpo  7141  acfun  7206  exmidontriimlem3  7222  exmidontriimlem4  7223  pw1ne1  7228  onntri35  7236  exmidapne  7259  ccfunen  7263  cc2lem  7265  elni2  7313  recexnq  7389  recmulnqg  7390  enq0enq  7430  enq0sym  7431  enq0ref  7432  enq0tr  7433  enq0breq  7435  nqnq0pi  7437  nqnq0  7440  prop  7474  prcdnql  7483  prcunqu  7484  prubl  7485  prltlu  7486  prnmaxl  7487  prnminu  7488  prdisj  7491  prarloc  7502  genipv  7508  genpelvl  7511  genpelvu  7512  genprndl  7520  genprndu  7521  distrlem5prl  7585  distrlem5pru  7586  ltexprlemm  7599  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  aptiprleml  7638  aptiprlemu  7639  archpr  7642  cauappcvgprlemm  7644  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  caucvgprlemm  7667  caucvgprlemladdfu  7676  caucvgprprlemmu  7694  elreal2  7829  ltresr  7838  axcnre  7880  axpre-suploclemres  7900  0re  7957  renepnf  8005  renemnf  8006  ltxrlt  8023  eqlei2  8052  0cnALT  8147  sup3exmid  8914  nn1suc  8938  nnne0  8947  xnn0xr  9244  nn0nepnf  9247  elz  9255  elnn0z  9266  elz2  9324  uzind4s  9590  elnn1uz2  9607  qre  9625  elpqb  9649  xnn0lenn0nn0  9865  xsubge0  9881  xposdif  9882  xleaddadd  9887  fzsn  10066  fz1sbc  10096  elfzp12  10099  fzm1  10100  fz01or  10111  fvinim0ffz  10241  flqidz  10286  ceilqidz  10316  modqmuladdnn0  10368  frec2uzrand  10405  frecuzrdgtcl  10412  fzfig  10430  seq3fveq2  10469  seq3shft2  10473  monoord  10476  seq3split  10479  iseqf1olemqval  10487  seq3id2  10509  1exp  10549  bcval  10729  hashennn  10760  zfz1isolem1  10820  zfz1iso  10821  seq3coll  10822  shftlem  10825  shftfibg  10829  shftfib  10832  shftfn  10833  2shfti  10840  rexuz3  10999  sqrt0rlem  11012  cau3  11124  negfi  11236  sumdc  11366  sumrbdclem  11385  summodclem2a  11389  fisumss  11400  prodrbdclem  11579  prodmodclem2a  11584  fprodssdc  11598  fprodsplit1f  11642  ef0lem  11668  odd2np1  11878  even2n  11879  oddnn02np1  11885  oddge22np1  11886  evennn02n  11887  evennn2n  11888  nn0enne  11907  divalgmod  11932  suprzubdc  11953  zsupssdc  11955  uzwodc  12038  lcmgcdlem  12077  cncongr1  12103  1nprm  12114  isprm2  12117  dvdsnprmd  12125  prmdc  12130  exprmfct  12138  nprmdvds1  12140  coprm  12144  prmdiveq  12236  prm23lt5  12263  pcpre1  12292  pc2dvds  12329  pcz  12331  pcmpt  12341  qexpz  12350  4sqlem2  12387  ennnfonelemhom  12416  ctiunctlemudc  12438  ssnnctlemct  12447  imasaddfnlemg  12735  ismgmid  12796  isgrpid2  12913  mhmlem  12978  eqgval  13082  dvdsrcl2  13268  nzrunit  13329  lringuplu  13337  dvdsrzring  13496  fiinopn  13507  istopon  13516  basis2  13551  eltg3  13560  tg2  13563  tgidm  13577  bastop  13578  bastop2  13587  topnex  13589  isopn3  13628  tgrest  13672  cnpval  13701  lmbr  13716  cnconst  13737  txbas  13761  uptx  13777  txdis1cn  13781  cnmpt12  13790  cnmpt22  13797  hmeocnvb  13821  xblm  13920  isxms2  13955  mopni  13985  blssioo  14048  dedekindeulemuub  14098  dedekindeulemeu  14103  dedekindicclemuub  14107  dedekindicclemeu  14112  ivthinclemlm  14115  ivthinclemum  14116  lgsfvalg  14409  lgsval2lem  14414  lgsdir2lem2  14433  2lgsoddprmlem2  14457  2lgsoddprmlem3  14462  2sqlem2  14465  2sqlem6  14470  2sqlem7  14471  2sqlem10  14475  elabgf0  14532  bj-rspgt  14541  cbvrald  14543  decidi  14550  sumdc2  14554  bdssex  14657  bj-inex  14662  bj-intnexr  14664  bj-unexg  14676  bj-d0clsepcl  14680  bj-nnelirr  14708  bj-nn0suc  14719  bj-inf2vnlem1  14725  bj-inf2vnlem2  14726  bj-inf2vnlem3  14727  bj-inf2vnlem4  14728  bj-nn0sucALT  14733  bj-findis  14734  trilpolemcl  14788