Theorem eleq12d 2309

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  cbvraldva2  2793  cbvrexdva2  2794  cdeqel  3047  ru  3050  sbceqbid  3058  sbcel12g  3162  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  onintexmid  4722  elvvuni  4841  elrnmpt1  5035  canth  6039  smoeq  6566  smores  6568  smores2  6570  iordsmo  6573  nnaordi  6786  nnaordr  6788  fvixp  6991  cbvixp  7003  mptelixpg  7022  opabfi  7253  exmidaclem  7570  cc1  7637  cc2lem  7638  cc3  7640  ltapig  7711  ltmpig  7712  fzsubel  10482  elfzp1b  10520  wrd2ind  11516  ennnfonelemg  13351  ennnfonelemp1  13354  ennnfonelemnn0  13370  ctiunctlemu1st  13382  ctiunctlemu2nd  13383  ctiunctlemudc  13385  ctiunctlemfo  13387  xpsfrnel  13723  ismgm  13735  mgm1  13748  issgrpd  13785  ismndd  13808  eqgfval  14083  prdsbasprj  14288  ringcl  14423  unitinvcl  14538  aprval  14699  aprap  14706  aprprop  14709  islmodd  14737  rspcl  14936  rnglidlmmgm  14941  zndvds  15092  istps  15275  tpspropd  15279  eltpsg  15283  isms  15696  mspropd  15721  cnlimci  15916  depindlem2  16970