Theorem eleq12d 2300

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)

Hypotheses

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eleq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eleq12d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Proof of Theorem eleq12d

Step	Hyp	Ref	Expression
1		eleq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
2	1	eleq2d 2299	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))
3		eleq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	eleq1d 2298	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  cbvraldva2  2772  cbvrexdva2  2773  cdeqel  3024  ru  3027  sbceqbid  3035  sbcel12g  3139  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  onintexmid  4665  elvvuni  4783  elrnmpt1  4975  canth  5958  smoeq  6442  smores  6444  smores2  6446  iordsmo  6449  nnaordi  6662  nnaordr  6664  fvixp  6858  cbvixp  6870  mptelixpg  6889  opabfi  7108  exmidaclem  7398  cc1  7459  cc2lem  7460  cc3  7462  ltapig  7533  ltmpig  7534  fzsubel  10264  elfzp1b  10301  wrd2ind  11263  ennnfonelemg  12982  ennnfonelemp1  12985  ennnfonelemnn0  13001  ctiunctlemu1st  13013  ctiunctlemu2nd  13014  ctiunctlemudc  13016  ctiunctlemfo  13018  prdsbasprj  13323  xpsfrnel  13385  ismgm  13398  mgm1  13411  issgrpd  13453  ismndd  13478  eqgfval  13767  ringcl  13984  unitinvcl  14095  aprval  14254  aprap  14258  islmodd  14265  rspcl  14463  rnglidlmmgm  14468  zndvds  14621  istps  14714  tpspropd  14718  eltpsg  14722  isms  15135  mspropd  15160  cnlimci  15355