Theorem eleq1 2256

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  eleq12  2258  eleq1i  2259  eleq1d  2262  eleq1a  2265  cleqh  2293  nelneq  2294  clelsb1  2298  nfcjust  2324  cleqf  2361  nelne2  2455  neleq1  2463  rgen2a  2548  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvrab  2758  eqvisset  2770  ceqsralt  2787  vtoclgaf  2825  vtocl2gaf  2827  vtocl3gaf  2829  rspct  2857  rspc  2858  rspce  2859  rspc2gv  2876  ceqsrexv  2890  ceqsrexbv  2891  clel2  2893  elabgt  2901  elabgf  2902  elrabi  2913  elrabf  2914  elrab3t  2915  ralab2  2924  rexab2  2926  mo2icl  2939  morex  2944  reu2  2948  reu6  2949  rmo4  2953  reu8  2956  reuind  2965  nelrdva  2967  ru  2984  dfsbcq  2987  dfsbcq2  2988  sbc8g  2993  sbcel1v  3048  rmob  3078  difjust  3154  unjust  3156  injust  3158  eldif  3162  dfss2f  3170  uniiunlem  3268  elun  3300  elin  3342  rabn0m  3474  disjne  3500  r19.3rm  3535  r19.9rmv  3538  raaanlem  3551  raaan  3552  ifmdc  3597  elpwg  3609  elpr2  3640  elsn2g  3651  rabsn  3685  tpid3g  3733  snssb  3751  snssgOLD  3754  difsn  3755  sssnm  3780  opeq1  3804  opeq2  3805  eluni  3838  elunii  3840  eluniab  3847  elint  3876  elintg  3878  elintab  3881  elintrabg  3883  intss1  3885  eliun  3916  eliin  3917  dfiunv2  3948  opabss  4093  cbvmpt  4124  trel  4134  trss  4136  ssex  4166  intnexr  4180  intexabim  4181  exmidel  4234  euabex  4254  elopab  4288  opelopab2a  4295  frirrg  4381  tz7.2  4385  ordelord  4412  onm  4432  ralxfr2d  4495  rexxfr2d  4496  rabxfrd  4500  reuhypd  4502  ordtriexmid  4553  ontriexmidim  4554  ordtri2orexmid  4555  ontr2exmid  4557  onsucsssucexmid  4559  onsucelsucexmid  4562  ordsucunielexmid  4563  regexmidlem1  4565  elirr  4573  nordeq  4576  sucprcreg  4581  en2lp  4586  ordsoexmid  4594  ordsuc  4595  onsucuni2  4596  tfis  4615  peano2  4627  findes  4635  limom  4646  opelxp  4689  opeliunxp  4714  opbrop  4738  ssrel  4747  ssrel2  4749  ssrelrel  4759  relopabi  4787  eliunxp  4801  opeliunxp2  4802  ideqg  4813  dmmrnm  4881  dmxpm  4882  elreldm  4888  elrnmptg  4914  elres  4978  resiexg  4987  dfres2  4994  imai  5021  elimasng  5033  issref  5048  xpmlem  5086  xpm  5087  elxp4  5153  elxp5  5154  unielrel  5193  relcnvexb  5205  dmfex  5443  funfveu  5567  funimass4  5607  fvelimab  5613  ssimaex  5618  fvopab3g  5630  fvopab3ig  5631  fvmptssdm  5642  chfnrn  5669  fvelrn  5689  fmpt  5708  ffnfv  5716  fmptco  5724  elunirn  5809  f1elima  5816  cbvriota  5884  acexmidlemab  5912  acexmidlemcase  5913  cbvmpox  5996  eloprabga  6005  resoprab  6014  elrnmpo  6032  ov  6038  ovig  6040  ov6g  6056  ovg  6057  ovelrn  6067  caovimo  6112  fo1stresm  6214  fo2ndresm  6215  elxp6  6222  unielxp  6227  eqop2  6231  dfoprab4  6245  dfoprab4f  6246  fmpox  6253  1stconst  6274  2ndconst  6275  f1o2ndf1  6281  xporderlem  6284  f1od2  6288  disjxp1  6289  opeliunxp2f  6291  dftpos3  6315  dftpos4  6316  tpostpos  6317  smoel  6353  tfr1onlemaccex  6401  tfrcllemaccex  6414  tfrcl  6417  frecabcl  6452  frecsuc  6460  nntri3or  6546  nntri3  6550  nndcel  6553  riinerm  6662  th3qlem1  6691  mapsncnv  6749  elixpsn  6789  dom2lem  6826  fiprc  6869  xpsnen  6875  phplem3g  6912  phpelm  6922  ssfiexmid  6932  domfiexmid  6934  inffiexmid  6962  undifdcss  6979  opabfi  6992  snon0  6994  f1dmvrnfibi  7003  f1vrnfibi  7004  ordiso2  7094  ctssdclemn0  7169  ctssdc  7172  enumct  7174  nnnninf  7185  nnnninfeq  7187  nninfisollemne  7190  nninfisol  7192  finomni  7199  exmidlpo  7202  acfun  7267  exmidontriimlem3  7283  exmidontriimlem4  7284  pw1ne1  7289  onntri35  7297  exmidapne  7320  ccfunen  7324  cc2lem  7326  elni2  7374  recexnq  7450  recmulnqg  7451  enq0enq  7491  enq0sym  7492  enq0ref  7493  enq0tr  7494  enq0breq  7496  nqnq0pi  7498  nqnq0  7501  prop  7535  prcdnql  7544  prcunqu  7545  prubl  7546  prltlu  7547  prnmaxl  7548  prnminu  7549  prdisj  7552  prarloc  7563  genipv  7569  genpelvl  7572  genpelvu  7573  genprndl  7581  genprndu  7582  distrlem5prl  7646  distrlem5pru  7647  ltexprlemm  7660  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  aptiprleml  7699  aptiprlemu  7700  archpr  7703  cauappcvgprlemm  7705  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemm  7728  caucvgprlemladdfu  7737  caucvgprprlemmu  7755  elreal2  7890  ltresr  7899  axcnre  7941  axpre-suploclemres  7961  0re  8019  renepnf  8067  renemnf  8068  ltxrlt  8085  eqlei2  8114  0cnALT  8209  sup3exmid  8976  nn1suc  9001  nnne0  9010  xnn0xr  9308  nn0nepnf  9311  elz  9319  elnn0z  9330  elz2  9388  uzind4s  9655  elnn1uz2  9672  qre  9690  elpqb  9715  xnn0lenn0nn0  9931  xsubge0  9947  xposdif  9948  xleaddadd  9953  fzsn  10132  fz1sbc  10162  elfzp12  10165  fzm1  10166  fz01or  10177  fvinim0ffz  10308  xqltnle  10336  flqidz  10355  ceilqidz  10387  modqmuladdnn0  10439  frec2uzrand  10476  frecuzrdgtcl  10483  fzfig  10501  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  seq3split  10559  seqsplitg  10560  iseqf1olemqval  10571  seq3id2  10597  seqhomog  10601  1exp  10639  bcval  10820  hashennn  10851  zfz1isolem1  10911  zfz1iso  10912  seq3coll  10913  iswrdiz  10921  0wrd0  10940  shftlem  10960  shftfibg  10964  shftfib  10967  shftfn  10968  2shfti  10975  rexuz3  11134  sqrt0rlem  11147  cau3  11259  negfi  11371  sumdc  11501  sumrbdclem  11520  summodclem2a  11524  fisumss  11535  prodrbdclem  11714  prodmodclem2a  11719  fprodssdc  11733  fprodsplit1f  11777  ef0lem  11803  odd2np1  12014  even2n  12015  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  nn0enne  12043  divalgmod  12068  suprzubdc  12089  zsupssdc  12091  uzwodc  12174  lcmgcdlem  12215  cncongr1  12241  1nprm  12252  isprm2  12255  dvdsnprmd  12263  prmdc  12268  exprmfct  12276  nprmdvds1  12278  coprm  12282  prmdiveq  12374  prm23lt5  12401  pcpre1  12430  pc2dvds  12468  pcz  12470  pcmpt  12481  qexpz  12490  4sqlem2  12527  4sqlem19  12547  ennnfonelemhom  12572  ctiunctlemudc  12594  ssnnctlemct  12603  nninfdclemcl  12605  imasaddfnlemg  12897  ismgmid  12960  isgrpid2  13112  mhmlem  13184  eqgval  13293  dvdsrcl2  13595  nzrunit  13684  lringuplu  13692  dvdsrzring  14091  znrrg  14148  fiinopn  14172  istopon  14181  basis2  14216  eltg3  14225  tg2  14228  tgidm  14242  bastop  14243  bastop2  14252  topnex  14254  isopn3  14293  tgrest  14337  cnpval  14366  lmbr  14381  cnconst  14402  txbas  14426  uptx  14442  txdis1cn  14446  cnmpt12  14455  cnmpt22  14462  hmeocnvb  14486  xblm  14585  isxms2  14620  mopni  14650  blssioo  14713  dedekindeulemuub  14771  dedekindeulemeu  14776  dedekindicclemuub  14780  dedekindicclemeu  14785  ivthinclemlm  14788  ivthinclemum  14789  ivthreinc  14799  lgsfvalg  15121  lgsval2lem  15126  lgsdir2lem2  15145  gausslemma2dlem1a  15174  gausslemma2dlem4  15180  gausslemma2dlem6  15183  2lgsoddprmlem2  15194  2lgsoddprmlem3  15199  2sqlem2  15202  2sqlem6  15207  2sqlem7  15208  2sqlem10  15212  elabgf0  15269  bj-rspgt  15278  cbvrald  15280  decidi  15287  sumdc2  15291  bdssex  15394  bj-inex  15399  bj-intnexr  15401  bj-unexg  15413  bj-d0clsepcl  15417  bj-nnelirr  15445  bj-nn0suc  15456  bj-inf2vnlem1  15462  bj-inf2vnlem2  15463  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465  bj-nn0sucALT  15470  bj-findis  15471  trilpolemcl  15527