Theorem eleq2 2241

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eleq2	⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2171	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1558	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	anbi2d 464	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	exbidv 1825	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2173	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2173	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1351   = 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  eleq2i  2244  eleq2d  2247  nelneq2  2279  clelsb2  2283  dvelimdc  2340  nelne1  2437  neleq2  2447  raleqf  2669  rexeqf  2670  reueq1f  2671  rmoeq1f  2672  rabeqf  2729  clel3g  2873  clel4  2875  sbcbi2  3015  sbcel2gv  3028  csbeq2  3083  sbnfc2  3119  difeq2  3249  uneq1  3284  ineq1  3331  nel02  3429  n0i  3430  disjel  3479  exsnrex  3636  sneqr  3762  preqr1g  3768  preqr1  3770  preq12b  3772  prel12  3773  elunii  3816  eluniab  3823  ssuni  3833  elinti  3855  elintab  3857  intss1  3861  intmin  3866  intab  3875  iineq2  3905  dfiin2g  3921  breq  4007  axsep2  4124  zfauscl  4125  inuni  4157  exmidexmid  4198  ss1o0el1  4199  exmid01  4200  exmidundif  4208  exmidundifim  4209  rext  4217  intid  4226  mss  4228  opth1  4238  opeqex  4251  frforeq3  4349  frirrg  4352  limeq  4379  nsuceq0g  4420  suctr  4423  snnex  4450  uniuni  4453  iunpw  4482  ordtriexmidlem  4520  ordtriexmidlem2  4521  ordtriexmid  4522  ontriexmidim  4523  ordtri2orexmid  4524  ontr2exmid  4526  ordtri2or2exmidlem  4527  onsucelsucexmidlem  4530  onsucelsucexmid  4531  ordsucunielexmid  4532  regexmidlem1  4534  reg2exmidlema  4535  regexmid  4536  reg2exmid  4537  elirr  4542  en2lp  4555  suc11g  4558  dtruex  4560  ordsoexmid  4563  nlimsucg  4567  onintexmid  4574  reg3exmidlemwe  4580  reg3exmid  4581  peano5  4599  limom  4615  0elnn  4620  nn0eln0  4621  nnregexmid  4622  xpeq1  4642  xpeq2  4643  opthprc  4679  xp11m  5069  funopg  5252  dffo4  5666  elunirn  5769  f1oiso  5829  canth  5831  eusvobj2  5863  acexmidlema  5868  acexmidlemb  5869  acexmidlemab  5871  acexmidlem2  5874  mpoeq123  5936  oprssdmm  6174  unielxp  6177  cnvf1o  6228  smoel  6303  tfr0dm  6325  frecabcl  6402  nnsucelsuc  6494  nntri3or  6496  nntri2  6497  nntri3  6500  nndceq  6502  nnmordi  6519  nnaordex  6531  elqsn0m  6605  qsel  6614  mapsn  6692  findcard2s  6892  undifdcss  6924  ctssdclemr  7113  nnnninf2  7127  exmidonfinlem  7194  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  exmidontriimlem3  7224  exmidontriimlem4  7225  exmidontriim  7226  pw1ne3  7231  sucpw1ne3  7233  sucpw1nel3  7234  onntri35  7238  elni2  7315  addnidpig  7337  elinp  7475  suplocexprlemdisj  7721  suplocexprlemub  7724  pitonn  7849  peano1nnnn  7853  peano2nnnn  7854  peano5nnnn  7893  sup3exmid  8916  peano5nni  8924  1nn  8932  peano2nn  8933  dfuzi  9365  uz11  9552  elfzonlteqm1  10212  frec2uzltd  10405  0tonninf  10441  1tonninf  10442  sumeq1  11365  prodeq1f  11562  ctiunct  12443  ssomct  12448  issubm  12868  isnsg  13067  releqgg  13085  issubrg  13347  lmodfopnelem2  13420  islssm  13450  istopg  13538  fiinbas  13588  topbas  13606  epttop  13629  restbasg  13707  icnpimaex  13750  lmcvg  13756  iscnp4  13757  cncnpi  13767  cnconst2  13772  cnptoprest  13778  cnptoprest2  13779  cnpdis  13781  lmss  13785  lmff  13788  txbas  13797  eltx  13798  txcnp  13810  txlm  13818  blssps  13966  blss  13967  blssexps  13968  blssex  13969  neibl  14030  metss  14033  metrest  14045  xmettx  14049  metcnp3  14050  tgioo  14085  tgqioo  14086  bdsep2  14677  bdzfauscl  14681  bj-indeq  14720  bj-nn0suc0  14741  bj-nnelirr  14744  bj-peano4  14746  bj-inf2vnlem2  14762  bj-nn0sucALT  14769  bj-findis  14770  strcollnft  14775  sscoll2  14779  nninfsellemdc  14798  nninfsellemqall  14803