Theorem eleq1 2295

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398  ∃wex 1541   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eleq12  2297  eleq1i  2298  eleq1d  2301  eleq1a  2304  cleqh  2332  nelneq  2333  clelsb1  2337  nfcjust  2372  cleqf  2409  nelne2  2503  neleq1  2511  rgen2a  2596  cbvralf  2769  cbvrexf  2770  cbvreu  2776  cbvrab  2811  eqvisset  2824  ceqsralt  2841  vtoclgaf  2880  vtocl2gaf  2882  vtocl3gaf  2884  rspct  2914  rspc  2915  rspce  2916  rspc2gv  2933  ceqsrexv  2947  ceqsrexbv  2948  clel2  2950  elabgt  2958  elabgf  2959  elrabi  2970  elrabf  2971  elrab3t  2972  ralab2  2981  rexab2  2983  mo2icl  2996  morex  3001  reu2  3005  reu6  3006  rmo4  3010  reu8  3013  reuind  3022  nelrdva  3024  ru  3041  dfsbcq  3044  dfsbcq2  3045  sbc8g  3050  sbcel1v  3105  rmob  3136  difjust  3212  unjust  3214  injust  3216  eldif  3220  dfss2f  3229  uniiunlem  3328  elun  3360  elin  3402  rabn0m  3536  disjne  3562  r19.3rm  3598  r19.9rmv  3601  raaanlem  3614  raaan  3615  elif  3634  ifmdc  3665  elpwg  3677  elpr2  3711  elsn2g  3722  rabsn  3756  tpid3g  3807  snssb  3827  snssgOLD  3830  difsn  3831  sssnm  3858  opeq1  3883  opeq2  3884  eluni  3917  elunii  3919  eluniab  3926  elint  3955  elintg  3957  elintab  3960  elintrabg  3962  intss1  3964  eliun  3995  eliin  3996  dfiunv2  4027  opabss  4174  cbvmpt  4205  trel  4215  trss  4217  ssex  4247  intnexr  4263  intexabim  4264  exmidel  4318  euabex  4341  elopab  4376  opelopab2a  4383  frirrg  4471  tz7.2  4475  ordelord  4502  onm  4522  ralxfr2d  4585  rexxfr2d  4586  rabxfrd  4590  reuhypd  4592  ordtriexmid  4643  ontriexmidim  4644  ordtri2orexmid  4645  ontr2exmid  4647  onsucsssucexmid  4649  onsucelsucexmid  4652  ordsucunielexmid  4653  regexmidlem1  4655  elirr  4663  nordeq  4666  sucprcreg  4671  en2lp  4676  ordsoexmid  4684  ordsuc  4685  onsucuni2  4686  tfis  4705  peano2  4717  findes  4725  limom  4736  opelxp  4779  opeliunxp  4805  opbrop  4829  ssrel  4838  ssrel2  4840  ssrelrel  4850  relopabi  4880  eliunxp  4894  opeliunxp2  4895  ideqg  4906  reldmm  4975  dmmrnm  4976  dmxpm  4977  elreldm  4983  elrnmptg  5009  elres  5074  resiexg  5083  dfres2  5090  imai  5118  elimasng  5130  issref  5145  xpmlem  5183  xpm  5184  elxp4  5250  elxp5  5251  unielrel  5290  relcnvexb  5302  dmfex  5557  funfveu  5683  funimass4  5727  fvelimab  5733  ssimaex  5738  fvopab3g  5750  fvopab3ig  5751  fvmptssdm  5762  chfnrn  5789  fvelrn  5808  fmpt  5827  ffnfv  5835  fmptco  5843  elunirn  5939  f1elima  5946  cbvriota  6015  acexmidlemab  6044  acexmidlemcase  6045  cbvmpox  6131  eloprabga  6140  resoprab  6149  elrnmpo  6167  ov  6173  ovig  6175  ov6g  6192  ovg  6193  ovelrn  6203  caovimo  6248  fo1stresm  6355  fo2ndresm  6356  elxp6  6363  unielxp  6368  eqop2  6372  dfoprab4  6386  dfoprab4f  6387  fmpox  6396  1stconst  6417  2ndconst  6418  f1o2ndf1  6424  xporderlem  6427  f1od2  6431  disjxp1  6432  opeliunxp2f  6469  dftpos3  6493  dftpos4  6494  tpostpos  6495  smoel  6531  tfr1onlemaccex  6579  tfrcllemaccex  6592  tfrcl  6595  frecabcl  6630  frecsuc  6638  nntri3or  6726  nntri3  6730  nndcel  6733  riinerm  6842  th3qlem1  6871  mapsncnv  6930  elixpsn  6970  dom2lem  7011  fiprc  7057  xpsnen  7072  phplem3g  7110  phpelm  7121  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  elssdc  7162  inffiexmid  7166  undifdcss  7183  opabfi  7200  snon0  7202  f1dmvrnfibi  7211  f1vrnfibi  7212  suppeqfsuppbi  7248  ordiso2  7326  ctssdclemn0  7401  ctssdc  7404  enumct  7406  nnnninf  7417  nnnninfeq  7419  nninfisollemne  7422  nninfisol  7424  finomni  7431  exmidlpo  7434  pr2cv1  7492  acneq  7509  finacn  7511  acfun  7514  exmidontriimlem3  7530  exmidontriimlem4  7531  pw1ne1  7539  onntri35  7547  exmidapne  7574  ccfunen  7578  cc2lem  7580  elni2  7629  recexnq  7705  recmulnqg  7706  enq0enq  7746  enq0sym  7747  enq0ref  7748  enq0tr  7749  enq0breq  7751  nqnq0pi  7753  nqnq0  7756  prop  7790  prcdnql  7799  prcunqu  7800  prubl  7801  prltlu  7802  prnmaxl  7803  prnminu  7804  prdisj  7807  prarloc  7818  genipv  7824  genpelvl  7827  genpelvu  7828  genprndl  7836  genprndu  7837  distrlem5prl  7901  distrlem5pru  7902  ltexprlemm  7915  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemrl  7925  ltexprlemru  7927  aptiprleml  7954  aptiprlemu  7955  archpr  7958  cauappcvgprlemm  7960  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  caucvgprlemm  7983  caucvgprlemladdfu  7992  caucvgprprlemmu  8010  elreal2  8145  ltresr  8154  axcnre  8196  axpre-suploclemres  8216  0re  8274  renepnf  8321  renemnf  8322  ltxrlt  8339  eqlei2  8368  0cnALT  8463  sup3exmid  9231  nn1suc  9256  nnne0  9265  xnn0xr  9568  nn0nepnf  9571  elz  9579  elnn0z  9590  elz2  9649  uzind4s  9922  elnn1uz2  9939  qre  9957  elpqb  9982  xnn0lenn0nn0  10198  xsubge0  10214  xposdif  10215  xleaddadd  10220  fzsn  10400  fz1sbc  10430  elfzp12  10433  fzm1  10434  fz01or  10445  fvinim0ffz  10587  suprzubdc  10596  zsupssdc  10598  xqltnle  10627  flqidz  10646  ceilqidz  10678  modqmuladdnn0  10730  frec2uzrand  10767  frecuzrdgtcl  10774  fzfig  10792  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  monoord  10847  seq3split  10850  seqsplitg  10851  iseqf1olemqval  10862  seq3id2  10888  seqhomog  10892  1exp  10930  bcval  11111  hashennn  11143  hashfibc  11207  zfz1isolem1  11212  zfz1iso  11213  seq3coll  11214  iswrdiz  11231  0wrd0  11250  lswlgt0cl  11277  ccatval1  11285  ccatval2  11286  ccatalpha  11301  ccatrcl1  11302  wrdl1s1  11318  ccats1val2  11328  wrd2ind  11415  pfxccatin12lem3  11424  pfxccatid  11433  reuccatpfxs1lem  11438  shftlem  11501  shftfibg  11505  shftfib  11508  shftfn  11509  2shfti  11516  rexuz3  11675  sqrt0rlem  11688  cau3  11800  negfi  11913  sumdc  12043  sumrbdclem  12063  summodclem2a  12067  fisumss  12078  prodrbdclem  12257  prodmodclem2a  12262  fprodssdc  12276  fprodsplit1f  12320  ef0lem  12346  odd2np1  12559  even2n  12560  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  nn0enne  12588  divalgmod  12613  uzwodc  12733  lcmgcdlem  12774  cncongr1  12800  1nprm  12811  isprm2  12814  dvdsnprmd  12822  prmdc  12827  exprmfct  12835  nprmdvds1  12837  coprm  12841  prmdiveq  12933  prm23lt5  12961  pcpre1  12990  pc2dvds  13028  pcz  13030  pcmpt  13041  qexpz  13050  4sqlem2  13087  4sqlem19  13107  ballotfilem2  13142  ennnfonelemhom  13166  ctiunctlemudc  13188  ssnnctlemct  13197  nninfdclemcl  13199  imasaddfnlemg  13527  ismgmid  13590  isgrpid2  13753  mhmlem  13831  eqgval  13940  dvdsrcl2  14244  nzrunit  14333  lringuplu  14341  dvdsrzring  14751  znrrg  14808  mplsubgfilemm  14853  fiinopn  14869  istopon  14878  basis2  14913  eltg3  14922  tg2  14925  tgidm  14939  bastop  14940  bastop2  14949  topnex  14951  isopn3  14990  tgrest  15034  cnpval  15063  lmbr  15078  cnconst  15099  txbas  15123  uptx  15139  txdis1cn  15143  cnmpt12  15152  cnmpt22  15159  hmeocnvb  15183  xblm  15282  isxms2  15317  mopni  15347  blssioo  15418  dedekindeulemuub  15482  dedekindeulemeu  15487  dedekindicclemuub  15491  dedekindicclemeu  15496  ivthinclemlm  15499  ivthinclemum  15500  ivthreinc  15510  pellexlem3  15847  lgsfvalg  15878  lgsval2lem  15883  lgsdir2lem2  15902  gausslemma2dlem1a  15931  gausslemma2dlem4  15937  gausslemma2dlem6  15940  2lgslem1b  15962  2lgs  15977  2lgsoddprmlem2  15979  2lgsoddprmlem3  15984  2sqlem2  15988  2sqlem6  15993  2sqlem7  15994  2sqlem10  15998  vtxvalg  16011  iedgvalg  16012  umgredg  16140  upgrpredgv  16141  usgredg2vlem2  16218  ushgredgedg  16221  ushgredgedgloop  16223  griedg0ssusgr  16246  uhgrspansubgrlem  16271  vtxdgfifival  16286  iswlk  16318  upgrwlkvtxedg  16359  isclwwlknx  16411  clwwlkn1loopb  16415  clwwlknonex2lem1  16432  elabgf0  16549  bj-rspgt  16558  cbvrald  16560  decidi  16567  sumdc2  16571  bdssex  16672  bj-inex  16677  bj-intnexr  16679  bj-unexg  16691  bj-d0clsepcl  16695  bj-nnelirr  16723  bj-nn0suc  16734  bj-inf2vnlem1  16740  bj-inf2vnlem2  16741  bj-inf2vnlem3  16742  bj-inf2vnlem4  16743  bj-nn0sucALT  16748  bj-findis  16749  3dom  16762  trilpolemcl  16821