Theorem eleq12d 2302

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  cbvraldva2  2774  cbvrexdva2  2775  cdeqel  3027  ru  3030  sbceqbid  3038  sbcel12g  3142  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  onintexmid  4671  elvvuni  4790  elrnmpt1  4983  canth  5969  smoeq  6456  smores  6458  smores2  6460  iordsmo  6463  nnaordi  6676  nnaordr  6678  fvixp  6872  cbvixp  6884  mptelixpg  6903  opabfi  7132  exmidaclem  7423  cc1  7484  cc2lem  7485  cc3  7487  ltapig  7558  ltmpig  7559  fzsubel  10295  elfzp1b  10332  wrd2ind  11308  ennnfonelemg  13029  ennnfonelemp1  13032  ennnfonelemnn0  13048  ctiunctlemu1st  13060  ctiunctlemu2nd  13061  ctiunctlemudc  13063  ctiunctlemfo  13065  prdsbasprj  13370  xpsfrnel  13432  ismgm  13445  mgm1  13458  issgrpd  13500  ismndd  13525  eqgfval  13814  ringcl  14032  unitinvcl  14143  aprval  14302  aprap  14306  islmodd  14313  rspcl  14511  rnglidlmmgm  14516  zndvds  14669  istps  14762  tpspropd  14766  eltpsg  14770  isms  15183  mspropd  15208  cnlimci  15403  depindlem2  16352