Theorem eleq1 2259

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364  ∃wex 1506   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12  2261  eleq1i  2262  eleq1d  2265  eleq1a  2268  cleqh  2296  nelneq  2297  clelsb1  2301  nfcjust  2327  cleqf  2364  nelne2  2458  neleq1  2466  rgen2a  2551  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrab  2761  eqvisset  2773  ceqsralt  2790  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  rspct  2861  rspc  2862  rspce  2863  rspc2gv  2880  ceqsrexv  2894  ceqsrexbv  2895  clel2  2897  elabgt  2905  elabgf  2906  elrabi  2917  elrabf  2918  elrab3t  2919  ralab2  2928  rexab2  2930  mo2icl  2943  morex  2948  reu2  2952  reu6  2953  rmo4  2957  reu8  2960  reuind  2969  nelrdva  2971  ru  2988  dfsbcq  2991  dfsbcq2  2992  sbc8g  2997  sbcel1v  3052  rmob  3082  difjust  3158  unjust  3160  injust  3162  eldif  3166  dfss2f  3174  uniiunlem  3272  elun  3304  elin  3346  rabn0m  3478  disjne  3504  r19.3rm  3539  r19.9rmv  3542  raaanlem  3555  raaan  3556  ifmdc  3601  elpwg  3613  elpr2  3644  elsn2g  3655  rabsn  3689  tpid3g  3737  snssb  3755  snssgOLD  3758  difsn  3759  sssnm  3784  opeq1  3808  opeq2  3809  eluni  3842  elunii  3844  eluniab  3851  elint  3880  elintg  3882  elintab  3885  elintrabg  3887  intss1  3889  eliun  3920  eliin  3921  dfiunv2  3952  opabss  4097  cbvmpt  4128  trel  4138  trss  4140  ssex  4170  intnexr  4184  intexabim  4185  exmidel  4238  euabex  4258  elopab  4292  opelopab2a  4299  frirrg  4385  tz7.2  4389  ordelord  4416  onm  4436  ralxfr2d  4499  rexxfr2d  4500  rabxfrd  4504  reuhypd  4506  ordtriexmid  4557  ontriexmidim  4558  ordtri2orexmid  4559  ontr2exmid  4561  onsucsssucexmid  4563  onsucelsucexmid  4566  ordsucunielexmid  4567  regexmidlem1  4569  elirr  4577  nordeq  4580  sucprcreg  4585  en2lp  4590  ordsoexmid  4598  ordsuc  4599  onsucuni2  4600  tfis  4619  peano2  4631  findes  4639  limom  4650  opelxp  4693  opeliunxp  4718  opbrop  4742  ssrel  4751  ssrel2  4753  ssrelrel  4763  relopabi  4791  eliunxp  4805  opeliunxp2  4806  ideqg  4817  dmmrnm  4885  dmxpm  4886  elreldm  4892  elrnmptg  4918  elres  4982  resiexg  4991  dfres2  4998  imai  5025  elimasng  5037  issref  5052  xpmlem  5090  xpm  5091  elxp4  5157  elxp5  5158  unielrel  5197  relcnvexb  5209  dmfex  5447  funfveu  5571  funimass4  5611  fvelimab  5617  ssimaex  5622  fvopab3g  5634  fvopab3ig  5635  fvmptssdm  5646  chfnrn  5673  fvelrn  5693  fmpt  5712  ffnfv  5720  fmptco  5728  elunirn  5813  f1elima  5820  cbvriota  5888  acexmidlemab  5916  acexmidlemcase  5917  cbvmpox  6000  eloprabga  6009  resoprab  6018  elrnmpo  6036  ov  6042  ovig  6044  ov6g  6061  ovg  6062  ovelrn  6072  caovimo  6117  fo1stresm  6219  fo2ndresm  6220  elxp6  6227  unielxp  6232  eqop2  6236  dfoprab4  6250  dfoprab4f  6251  fmpox  6258  1stconst  6279  2ndconst  6280  f1o2ndf1  6286  xporderlem  6289  f1od2  6293  disjxp1  6294  opeliunxp2f  6296  dftpos3  6320  dftpos4  6321  tpostpos  6322  smoel  6358  tfr1onlemaccex  6406  tfrcllemaccex  6419  tfrcl  6422  frecabcl  6457  frecsuc  6465  nntri3or  6551  nntri3  6555  nndcel  6558  riinerm  6667  th3qlem1  6696  mapsncnv  6754  elixpsn  6794  dom2lem  6831  fiprc  6874  xpsnen  6880  phplem3g  6917  phpelm  6927  ssfiexmid  6937  domfiexmid  6939  inffiexmid  6967  undifdcss  6984  opabfi  6999  snon0  7001  f1dmvrnfibi  7010  f1vrnfibi  7011  ordiso2  7101  ctssdclemn0  7176  ctssdc  7179  enumct  7181  nnnninf  7192  nnnninfeq  7194  nninfisollemne  7197  nninfisol  7199  finomni  7206  exmidlpo  7209  acfun  7274  exmidontriimlem3  7290  exmidontriimlem4  7291  pw1ne1  7296  onntri35  7304  exmidapne  7327  ccfunen  7331  cc2lem  7333  elni2  7381  recexnq  7457  recmulnqg  7458  enq0enq  7498  enq0sym  7499  enq0ref  7500  enq0tr  7501  enq0breq  7503  nqnq0pi  7505  nqnq0  7508  prop  7542  prcdnql  7551  prcunqu  7552  prubl  7553  prltlu  7554  prnmaxl  7555  prnminu  7556  prdisj  7559  prarloc  7570  genipv  7576  genpelvl  7579  genpelvu  7580  genprndl  7588  genprndu  7589  distrlem5prl  7653  distrlem5pru  7654  ltexprlemm  7667  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  aptiprleml  7706  aptiprlemu  7707  archpr  7710  cauappcvgprlemm  7712  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemm  7735  caucvgprlemladdfu  7744  caucvgprprlemmu  7762  elreal2  7897  ltresr  7906  axcnre  7948  axpre-suploclemres  7968  0re  8026  renepnf  8074  renemnf  8075  ltxrlt  8092  eqlei2  8121  0cnALT  8216  sup3exmid  8984  nn1suc  9009  nnne0  9018  xnn0xr  9317  nn0nepnf  9320  elz  9328  elnn0z  9339  elz2  9397  uzind4s  9664  elnn1uz2  9681  qre  9699  elpqb  9724  xnn0lenn0nn0  9940  xsubge0  9956  xposdif  9957  xleaddadd  9962  fzsn  10141  fz1sbc  10171  elfzp12  10174  fzm1  10175  fz01or  10186  fvinim0ffz  10317  suprzubdc  10326  zsupssdc  10328  xqltnle  10357  flqidz  10376  ceilqidz  10408  modqmuladdnn0  10460  frec2uzrand  10497  frecuzrdgtcl  10504  fzfig  10522  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  iseqf1olemqval  10592  seq3id2  10618  seqhomog  10622  1exp  10660  bcval  10841  hashennn  10872  zfz1isolem1  10932  zfz1iso  10933  seq3coll  10934  iswrdiz  10942  0wrd0  10961  shftlem  10981  shftfibg  10985  shftfib  10988  shftfn  10989  2shfti  10996  rexuz3  11155  sqrt0rlem  11168  cau3  11280  negfi  11393  sumdc  11523  sumrbdclem  11542  summodclem2a  11546  fisumss  11557  prodrbdclem  11736  prodmodclem2a  11741  fprodssdc  11755  fprodsplit1f  11799  ef0lem  11825  odd2np1  12038  even2n  12039  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  nn0enne  12067  divalgmod  12092  uzwodc  12204  lcmgcdlem  12245  cncongr1  12271  1nprm  12282  isprm2  12285  dvdsnprmd  12293  prmdc  12298  exprmfct  12306  nprmdvds1  12308  coprm  12312  prmdiveq  12404  prm23lt5  12432  pcpre1  12461  pc2dvds  12499  pcz  12501  pcmpt  12512  qexpz  12521  4sqlem2  12558  4sqlem19  12578  ennnfonelemhom  12632  ctiunctlemudc  12654  ssnnctlemct  12663  nninfdclemcl  12665  imasaddfnlemg  12957  ismgmid  13020  isgrpid2  13172  mhmlem  13244  eqgval  13353  dvdsrcl2  13655  nzrunit  13744  lringuplu  13752  dvdsrzring  14159  znrrg  14216  fiinopn  14240  istopon  14249  basis2  14284  eltg3  14293  tg2  14296  tgidm  14310  bastop  14311  bastop2  14320  topnex  14322  isopn3  14361  tgrest  14405  cnpval  14434  lmbr  14449  cnconst  14470  txbas  14494  uptx  14510  txdis1cn  14514  cnmpt12  14523  cnmpt22  14530  hmeocnvb  14554  xblm  14653  isxms2  14688  mopni  14718  blssioo  14789  dedekindeulemuub  14853  dedekindeulemeu  14858  dedekindicclemuub  14862  dedekindicclemeu  14867  ivthinclemlm  14870  ivthinclemum  14871  ivthreinc  14881  lgsfvalg  15246  lgsval2lem  15251  lgsdir2lem2  15270  gausslemma2dlem1a  15299  gausslemma2dlem4  15305  gausslemma2dlem6  15308  2lgslem1b  15330  2lgs  15345  2lgsoddprmlem2  15347  2lgsoddprmlem3  15352  2sqlem2  15356  2sqlem6  15361  2sqlem7  15362  2sqlem10  15366  elabgf0  15423  bj-rspgt  15432  cbvrald  15434  decidi  15441  sumdc2  15445  bdssex  15548  bj-inex  15553  bj-intnexr  15555  bj-unexg  15567  bj-d0clsepcl  15571  bj-nnelirr  15599  bj-nn0suc  15610  bj-inf2vnlem1  15616  bj-inf2vnlem2  15617  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619  bj-nn0sucALT  15624  bj-findis  15625  trilpolemcl  15681