Theorem eleq12d 2277

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 2276	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))
3		eleq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	eleq1d 2275	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ 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:  cbvraldva2  2746  cbvrexdva2  2747  cdeqel  2996  ru  2999  sbceqbid  3007  sbcel12g  3110  cbvralcsf  3158  cbvrexcsf  3159  cbvreucsf  3160  cbvrabcsf  3161  onintexmid  4626  elvvuni  4744  elrnmpt1  4935  canth  5907  smoeq  6386  smores  6388  smores2  6390  iordsmo  6393  nnaordi  6604  nnaordr  6606  fvixp  6800  cbvixp  6812  mptelixpg  6831  opabfi  7047  exmidaclem  7333  cc1  7390  cc2lem  7391  cc3  7393  ltapig  7464  ltmpig  7465  fzsubel  10195  elfzp1b  10232  ennnfonelemg  12824  ennnfonelemp1  12827  ennnfonelemnn0  12843  ctiunctlemu1st  12855  ctiunctlemu2nd  12856  ctiunctlemudc  12858  ctiunctlemfo  12860  prdsbasprj  13164  xpsfrnel  13226  ismgm  13239  mgm1  13252  issgrpd  13294  ismndd  13319  eqgfval  13608  ringcl  13825  unitinvcl  13935  aprval  14094  aprap  14098  islmodd  14105  rspcl  14303  rnglidlmmgm  14308  zndvds  14461  istps  14554  tpspropd  14558  eltpsg  14562  isms  14975  mspropd  15000  cnlimci  15195