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  2696  cbvrexf  2697  cbvreu  2701  cbvrab  2735  eqvisset  2747  ceqsralt  2764  vtoclgaf  2802  vtocl2gaf  2804  vtocl3gaf  2806  rspct  2834  rspc  2835  rspce  2836  rspc2gv  2853  ceqsrexv  2867  ceqsrexbv  2868  clel2  2870  elabgt  2878  elabgf  2879  elrabi  2890  elrabf  2891  elrab3t  2892  ralab2  2901  rexab2  2903  mo2icl  2916  morex  2921  reu2  2925  reu6  2926  rmo4  2930  reu8  2933  reuind  2942  nelrdva  2944  ru  2961  dfsbcq  2964  dfsbcq2  2965  sbc8g  2970  sbcel1v  3025  rmob  3055  difjust  3130  unjust  3132  injust  3134  eldif  3138  dfss2f  3146  uniiunlem  3244  elun  3276  elin  3318  rabn0m  3450  disjne  3476  r19.3rm  3511  r19.9rmv  3514  raaanlem  3528  raaan  3529  ifmdc  3574  elpwg  3583  elpr2  3614  elsn2g  3625  rabsn  3659  tpid3g  3707  snssb  3725  snssgOLD  3728  difsn  3729  sssnm  3754  opeq1  3778  opeq2  3779  eluni  3812  elunii  3814  eluniab  3821  elint  3850  elintg  3852  elintab  3855  elintrabg  3857  intss1  3859  eliun  3890  eliin  3891  dfiunv2  3922  opabss  4067  cbvmpt  4098  trel  4108  trss  4110  ssex  4140  intnexr  4151  intexabim  4152  exmidel  4205  euabex  4225  elopab  4258  opelopab2a  4265  frirrg  4350  tz7.2  4354  ordelord  4381  onm  4401  ralxfr2d  4464  rexxfr2d  4465  rabxfrd  4469  reuhypd  4471  ordtriexmid  4520  ontriexmidim  4521  ordtri2orexmid  4522  ontr2exmid  4524  onsucsssucexmid  4526  onsucelsucexmid  4529  ordsucunielexmid  4530  regexmidlem1  4532  elirr  4540  nordeq  4543  sucprcreg  4548  en2lp  4553  ordsoexmid  4561  ordsuc  4562  onsucuni2  4563  tfis  4582  peano2  4594  findes  4602  limom  4613  opelxp  4656  opeliunxp  4681  opbrop  4705  ssrel  4714  ssrel2  4716  ssrelrel  4726  relopabi  4752  eliunxp  4766  opeliunxp2  4767  ideqg  4778  dmmrnm  4846  dmxpm  4847  elreldm  4853  elrnmptg  4879  elres  4943  resiexg  4952  dfres2  4959  imai  4984  elimasng  4996  issref  5011  xpmlem  5049  xpm  5050  elxp4  5116  elxp5  5117  unielrel  5156  relcnvexb  5168  dmfex  5405  funfveu  5528  funimass4  5566  fvelimab  5572  ssimaex  5577  fvopab3g  5589  fvopab3ig  5590  fvmptssdm  5600  chfnrn  5627  fvelrn  5647  fmpt  5666  ffnfv  5674  fmptco  5682  elunirn  5766  f1elima  5773  cbvriota  5840  acexmidlemab  5868  acexmidlemcase  5869  cbvmpox  5952  eloprabga  5961  resoprab  5970  elrnmpo  5987  ov  5993  ovig  5995  ov6g  6011  ovg  6012  ovelrn  6022  caovimo  6067  fo1stresm  6161  fo2ndresm  6162  elxp6  6169  unielxp  6174  eqop2  6178  dfoprab4  6192  dfoprab4f  6193  fmpox  6200  1stconst  6221  2ndconst  6222  f1o2ndf1  6228  xporderlem  6231  f1od2  6235  disjxp1  6236  opeliunxp2f  6238  dftpos3  6262  dftpos4  6263  tpostpos  6264  smoel  6300  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfrcl  6364  frecabcl  6399  frecsuc  6407  nntri3or  6493  nntri3  6497  nndcel  6500  riinerm  6607  th3qlem1  6636  mapsncnv  6694  elixpsn  6734  dom2lem  6771  fiprc  6814  xpsnen  6820  phplem3g  6855  phpelm  6865  ssfiexmid  6875  domfiexmid  6877  inffiexmid  6905  undifdcss  6921  snon0  6934  f1dmvrnfibi  6942  f1vrnfibi  6943  ordiso2  7033  ctssdclemn0  7108  ctssdc  7111  enumct  7113  nnnninf  7123  nnnninfeq  7125  nninfisollemne  7128  nninfisol  7130  finomni  7137  exmidlpo  7140  acfun  7205  exmidontriimlem3  7221  exmidontriimlem4  7222  pw1ne1  7227  onntri35  7235  exmidapne  7258  ccfunen  7262  cc2lem  7264  elni2  7312  recexnq  7388  recmulnqg  7389  enq0enq  7429  enq0sym  7430  enq0ref  7431  enq0tr  7432  enq0breq  7434  nqnq0pi  7436  nqnq0  7439  prop  7473  prcdnql  7482  prcunqu  7483  prubl  7484  prltlu  7485  prnmaxl  7486  prnminu  7487  prdisj  7490  prarloc  7501  genipv  7507  genpelvl  7510  genpelvu  7511  genprndl  7519  genprndu  7520  distrlem5prl  7584  distrlem5pru  7585  ltexprlemm  7598  ltexprlemdisj  7604  ltexprlemloc  7605  ltexprlemrl  7608  ltexprlemru  7610  aptiprleml  7637  aptiprlemu  7638  archpr  7641  cauappcvgprlemm  7643  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  caucvgprlemm  7666  caucvgprlemladdfu  7675  caucvgprprlemmu  7693  elreal2  7828  ltresr  7837  axcnre  7879  axpre-suploclemres  7899  0re  7956  renepnf  8004  renemnf  8005  ltxrlt  8022  eqlei2  8051  0cnALT  8146  sup3exmid  8913  nn1suc  8937  nnne0  8946  xnn0xr  9243  nn0nepnf  9246  elz  9254  elnn0z  9265  elz2  9323  uzind4s  9589  elnn1uz2  9606  qre  9624  elpqb  9648  xnn0lenn0nn0  9864  xsubge0  9880  xposdif  9881  xleaddadd  9886  fzsn  10065  fz1sbc  10095  elfzp12  10098  fzm1  10099  fz01or  10110  fvinim0ffz  10240  flqidz  10285  ceilqidz  10315  modqmuladdnn0  10367  frec2uzrand  10404  frecuzrdgtcl  10411  fzfig  10429  seq3fveq2  10468  seq3shft2  10472  monoord  10475  seq3split  10478  iseqf1olemqval  10486  seq3id2  10508  1exp  10548  bcval  10728  hashennn  10759  zfz1isolem1  10819  zfz1iso  10820  seq3coll  10821  shftlem  10824  shftfibg  10828  shftfib  10831  shftfn  10832  2shfti  10839  rexuz3  10998  sqrt0rlem  11011  cau3  11123  negfi  11235  sumdc  11365  sumrbdclem  11384  summodclem2a  11388  fisumss  11399  prodrbdclem  11578  prodmodclem2a  11583  fprodssdc  11597  fprodsplit1f  11641  ef0lem  11667  odd2np1  11877  even2n  11878  oddnn02np1  11884  oddge22np1  11885  evennn02n  11886  evennn2n  11887  nn0enne  11906  divalgmod  11931  suprzubdc  11952  zsupssdc  11954  uzwodc  12037  lcmgcdlem  12076  cncongr1  12102  1nprm  12113  isprm2  12116  dvdsnprmd  12124  prmdc  12129  exprmfct  12137  nprmdvds1  12139  coprm  12143  prmdiveq  12235  prm23lt5  12262  pcpre1  12291  pc2dvds  12328  pcz  12330  pcmpt  12340  qexpz  12349  4sqlem2  12386  ennnfonelemhom  12415  ctiunctlemudc  12437  ssnnctlemct  12446  imasaddfnlemg  12734  ismgmid  12795  isgrpid2  12912  mhmlem  12977  eqgval  13080  dvdsrcl2  13266  nzrunit  13327  lringuplu  13335  dvdsrzring  13463  fiinopn  13474  istopon  13483  basis2  13518  eltg3  13527  tg2  13530  tgidm  13544  bastop  13545  bastop2  13554  topnex  13556  isopn3  13595  tgrest  13639  cnpval  13668  lmbr  13683  cnconst  13704  txbas  13728  uptx  13744  txdis1cn  13748  cnmpt12  13757  cnmpt22  13764  hmeocnvb  13788  xblm  13887  isxms2  13922  mopni  13952  blssioo  14015  dedekindeulemuub  14065  dedekindeulemeu  14070  dedekindicclemuub  14074  dedekindicclemeu  14079  ivthinclemlm  14082  ivthinclemum  14083  lgsfvalg  14376  lgsval2lem  14381  lgsdir2lem2  14400  2lgsoddprmlem2  14424  2lgsoddprmlem3  14429  2sqlem2  14432  2sqlem6  14437  2sqlem7  14438  2sqlem10  14442  elabgf0  14499  bj-rspgt  14508  cbvrald  14510  decidi  14517  sumdc2  14521  bdssex  14624  bj-inex  14629  bj-intnexr  14631  bj-unexg  14643  bj-d0clsepcl  14647  bj-nnelirr  14675  bj-nn0suc  14686  bj-inf2vnlem1  14692  bj-inf2vnlem2  14693  bj-inf2vnlem3  14694  bj-inf2vnlem4  14695  bj-nn0sucALT  14700  bj-findis  14701  trilpolemcl  14755