Theorem eleq12d 2305

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

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

This theorem is referenced by:  cbvraldva2  2787  cbvrexdva2  2788  cdeqel  3041  ru  3044  sbceqbid  3052  sbcel12g  3156  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  onintexmid  4700  elvvuni  4819  elrnmpt1  5013  canth  6009  smoeq  6534  smores  6536  smores2  6538  iordsmo  6541  nnaordi  6754  nnaordr  6756  fvixp  6951  cbvixp  6963  mptelixpg  6982  opabfi  7213  exmidaclem  7528  cc1  7595  cc2lem  7596  cc3  7598  ltapig  7669  ltmpig  7670  fzsubel  10415  elfzp1b  10453  wrd2ind  11440  ennnfonelemg  13238  ennnfonelemp1  13241  ennnfonelemnn0  13257  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunctlemfo  13274  prdsbasprj  13579  xpsfrnel  13641  ismgm  13654  mgm1  13667  issgrpd  13709  ismndd  13734  eqgfval  14023  ringcl  14241  unitinvcl  14353  aprval  14514  aprap  14521  aprprop  14524  islmodd  14553  rspcl  14751  rnglidlmmgm  14756  zndvds  14909  istps  15009  tpspropd  15013  eltpsg  15017  isms  15430  mspropd  15455  cnlimci  15650  depindlem2  16614