Theorem eleq1 2269

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1373  ∃wex 1516   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eleq12  2271  eleq1i  2272  eleq1d  2275  eleq1a  2278  cleqh  2306  nelneq  2307  clelsb1  2311  nfcjust  2337  cleqf  2374  nelne2  2468  neleq1  2476  rgen2a  2561  cbvralf  2731  cbvrexf  2732  cbvreu  2737  cbvrab  2771  eqvisset  2784  ceqsralt  2801  vtoclgaf  2840  vtocl2gaf  2842  vtocl3gaf  2844  rspct  2874  rspc  2875  rspce  2876  rspc2gv  2893  ceqsrexv  2907  ceqsrexbv  2908  clel2  2910  elabgt  2918  elabgf  2919  elrabi  2930  elrabf  2931  elrab3t  2932  ralab2  2941  rexab2  2943  mo2icl  2956  morex  2961  reu2  2965  reu6  2966  rmo4  2970  reu8  2973  reuind  2982  nelrdva  2984  ru  3001  dfsbcq  3004  dfsbcq2  3005  sbc8g  3010  sbcel1v  3065  rmob  3095  difjust  3171  unjust  3173  injust  3175  eldif  3179  dfss2f  3188  uniiunlem  3286  elun  3318  elin  3360  rabn0m  3492  disjne  3518  r19.3rm  3553  r19.9rmv  3556  raaanlem  3569  raaan  3570  elif  3587  ifmdc  3617  elpwg  3629  elpr2  3660  elsn2g  3671  rabsn  3705  tpid3g  3753  snssb  3772  snssgOLD  3775  difsn  3776  sssnm  3801  opeq1  3825  opeq2  3826  eluni  3859  elunii  3861  eluniab  3868  elint  3897  elintg  3899  elintab  3902  elintrabg  3904  intss1  3906  eliun  3937  eliin  3938  dfiunv2  3969  opabss  4116  cbvmpt  4147  trel  4157  trss  4159  ssex  4189  intnexr  4203  intexabim  4204  exmidel  4257  euabex  4277  elopab  4312  opelopab2a  4319  frirrg  4405  tz7.2  4409  ordelord  4436  onm  4456  ralxfr2d  4519  rexxfr2d  4520  rabxfrd  4524  reuhypd  4526  ordtriexmid  4577  ontriexmidim  4578  ordtri2orexmid  4579  ontr2exmid  4581  onsucsssucexmid  4583  onsucelsucexmid  4586  ordsucunielexmid  4587  regexmidlem1  4589  elirr  4597  nordeq  4600  sucprcreg  4605  en2lp  4610  ordsoexmid  4618  ordsuc  4619  onsucuni2  4620  tfis  4639  peano2  4651  findes  4659  limom  4670  opelxp  4713  opeliunxp  4738  opbrop  4762  ssrel  4771  ssrel2  4773  ssrelrel  4783  relopabi  4811  eliunxp  4825  opeliunxp2  4826  ideqg  4837  dmmrnm  4906  dmxpm  4907  elreldm  4913  elrnmptg  4939  elres  5004  resiexg  5013  dfres2  5020  imai  5047  elimasng  5059  issref  5074  xpmlem  5112  xpm  5113  elxp4  5179  elxp5  5180  unielrel  5219  relcnvexb  5231  dmfex  5477  funfveu  5602  funimass4  5642  fvelimab  5648  ssimaex  5653  fvopab3g  5665  fvopab3ig  5666  fvmptssdm  5677  chfnrn  5704  fvelrn  5724  fmpt  5743  ffnfv  5751  fmptco  5759  elunirn  5848  f1elima  5855  cbvriota  5923  acexmidlemab  5951  acexmidlemcase  5952  cbvmpox  6036  eloprabga  6045  resoprab  6054  elrnmpo  6072  ov  6078  ovig  6080  ov6g  6097  ovg  6098  ovelrn  6108  caovimo  6153  fo1stresm  6260  fo2ndresm  6261  elxp6  6268  unielxp  6273  eqop2  6277  dfoprab4  6291  dfoprab4f  6292  fmpox  6299  1stconst  6320  2ndconst  6321  f1o2ndf1  6327  xporderlem  6330  f1od2  6334  disjxp1  6335  opeliunxp2f  6337  dftpos3  6361  dftpos4  6362  tpostpos  6363  smoel  6399  tfr1onlemaccex  6447  tfrcllemaccex  6460  tfrcl  6463  frecabcl  6498  frecsuc  6506  nntri3or  6592  nntri3  6596  nndcel  6599  riinerm  6708  th3qlem1  6737  mapsncnv  6795  elixpsn  6835  dom2lem  6876  fiprc  6921  xpsnen  6931  phplem3g  6968  phpelm  6978  ssfiexmid  6988  domfiexmid  6990  inffiexmid  7018  undifdcss  7035  opabfi  7050  snon0  7052  f1dmvrnfibi  7061  f1vrnfibi  7062  ordiso2  7152  ctssdclemn0  7227  ctssdc  7230  enumct  7232  nnnninf  7243  nnnninfeq  7245  nninfisollemne  7248  nninfisol  7250  finomni  7257  exmidlpo  7260  acneq  7330  finacn  7332  acfun  7335  exmidontriimlem3  7351  exmidontriimlem4  7352  pw1ne1  7360  onntri35  7368  exmidapne  7392  ccfunen  7396  cc2lem  7398  elni2  7447  recexnq  7523  recmulnqg  7524  enq0enq  7564  enq0sym  7565  enq0ref  7566  enq0tr  7567  enq0breq  7569  nqnq0pi  7571  nqnq0  7574  prop  7608  prcdnql  7617  prcunqu  7618  prubl  7619  prltlu  7620  prnmaxl  7621  prnminu  7622  prdisj  7625  prarloc  7636  genipv  7642  genpelvl  7645  genpelvu  7646  genprndl  7654  genprndu  7655  distrlem5prl  7719  distrlem5pru  7720  ltexprlemm  7733  ltexprlemdisj  7739  ltexprlemloc  7740  ltexprlemrl  7743  ltexprlemru  7745  aptiprleml  7772  aptiprlemu  7773  archpr  7776  cauappcvgprlemm  7778  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  caucvgprlemm  7801  caucvgprlemladdfu  7810  caucvgprprlemmu  7828  elreal2  7963  ltresr  7972  axcnre  8014  axpre-suploclemres  8034  0re  8092  renepnf  8140  renemnf  8141  ltxrlt  8158  eqlei2  8187  0cnALT  8282  sup3exmid  9050  nn1suc  9075  nnne0  9084  xnn0xr  9383  nn0nepnf  9386  elz  9394  elnn0z  9405  elz2  9464  uzind4s  9731  elnn1uz2  9748  qre  9766  elpqb  9791  xnn0lenn0nn0  10007  xsubge0  10023  xposdif  10024  xleaddadd  10029  fzsn  10208  fz1sbc  10238  elfzp12  10241  fzm1  10242  fz01or  10253  fvinim0ffz  10392  suprzubdc  10401  zsupssdc  10403  xqltnle  10432  flqidz  10451  ceilqidz  10483  modqmuladdnn0  10535  frec2uzrand  10572  frecuzrdgtcl  10579  fzfig  10597  seq3fveq2  10642  seqfveq2g  10644  seq3shft2  10648  seqshft2g  10649  monoord  10652  seq3split  10655  seqsplitg  10656  iseqf1olemqval  10667  seq3id2  10693  seqhomog  10697  1exp  10735  bcval  10916  hashennn  10947  zfz1isolem1  11007  zfz1iso  11008  seq3coll  11009  iswrdiz  11023  0wrd0  11042  lswlgt0cl  11068  ccatval1  11076  ccatval2  11077  wrdl1s1  11107  ccats1val2  11115  wrd2ind  11199  shftlem  11202  shftfibg  11206  shftfib  11209  shftfn  11210  2shfti  11217  rexuz3  11376  sqrt0rlem  11389  cau3  11501  negfi  11614  sumdc  11744  sumrbdclem  11763  summodclem2a  11767  fisumss  11778  prodrbdclem  11957  prodmodclem2a  11962  fprodssdc  11976  fprodsplit1f  12020  ef0lem  12046  odd2np1  12259  even2n  12260  oddnn02np1  12266  oddge22np1  12267  evennn02n  12268  evennn2n  12269  nn0enne  12288  divalgmod  12313  uzwodc  12433  lcmgcdlem  12474  cncongr1  12500  1nprm  12511  isprm2  12514  dvdsnprmd  12522  prmdc  12527  exprmfct  12535  nprmdvds1  12537  coprm  12541  prmdiveq  12633  prm23lt5  12661  pcpre1  12690  pc2dvds  12728  pcz  12730  pcmpt  12741  qexpz  12750  4sqlem2  12787  4sqlem19  12807  ennnfonelemhom  12861  ctiunctlemudc  12883  ssnnctlemct  12892  nninfdclemcl  12894  imasaddfnlemg  13221  ismgmid  13284  isgrpid2  13447  mhmlem  13525  eqgval  13634  dvdsrcl2  13936  nzrunit  14025  lringuplu  14033  dvdsrzring  14440  znrrg  14497  mplsubgfilemm  14535  fiinopn  14551  istopon  14560  basis2  14595  eltg3  14604  tg2  14607  tgidm  14621  bastop  14622  bastop2  14631  topnex  14633  isopn3  14672  tgrest  14716  cnpval  14745  lmbr  14760  cnconst  14781  txbas  14805  uptx  14821  txdis1cn  14825  cnmpt12  14834  cnmpt22  14841  hmeocnvb  14865  xblm  14964  isxms2  14999  mopni  15029  blssioo  15100  dedekindeulemuub  15164  dedekindeulemeu  15169  dedekindicclemuub  15173  dedekindicclemeu  15178  ivthinclemlm  15181  ivthinclemum  15182  ivthreinc  15192  lgsfvalg  15557  lgsval2lem  15562  lgsdir2lem2  15581  gausslemma2dlem1a  15610  gausslemma2dlem4  15616  gausslemma2dlem6  15619  2lgslem1b  15641  2lgs  15656  2lgsoddprmlem2  15658  2lgsoddprmlem3  15663  2sqlem2  15667  2sqlem6  15672  2sqlem7  15673  2sqlem10  15677  vtxvalg  15690  iedgvalg  15691  elabgf0  15852  bj-rspgt  15861  cbvrald  15863  decidi  15870  sumdc2  15874  bdssex  15976  bj-inex  15981  bj-intnexr  15983  bj-unexg  15995  bj-d0clsepcl  15999  bj-nnelirr  16027  bj-nn0suc  16038  bj-inf2vnlem1  16044  bj-inf2vnlem2  16045  bj-inf2vnlem3  16046  bj-inf2vnlem4  16047  bj-nn0sucALT  16052  bj-findis  16053  trilpolemcl  16117