Theorem vtocl2ga 3247

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.)

Hypotheses

Ref	Expression
vtocl2ga.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtocl2ga.2	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
vtocl2ga.3	⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)

Assertion

Ref	Expression
vtocl2ga	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝜓,𝑥   𝜒,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)   𝐵(𝑥)

Proof of Theorem vtocl2ga

Step	Hyp	Ref	Expression
1		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2751	. 2 ⊢ Ⅎ𝑦𝐴
3		nfcv 2751	. 2 ⊢ Ⅎ𝑦𝐵
4		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜓
5		nfv 1830	. 2 ⊢ Ⅎ𝑦𝜒
6		vtocl2ga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7		vtocl2ga.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
8		vtocl2ga.3	. 2 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)
9	1, 2, 3, 4, 5, 6, 7, 8	vtocl2gaf 3246	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175

This theorem is referenced by:  solin  4982  caovcan  6736  pwfseqlem2  9360  mulcanenq  9661  ltaddnq  9675  ltrnq  9680  genpv  9700  wrdind  13328  fsumrelem  14380  imasleval  16024  fullfunc  16389  fthfunc  16390  pf1ind  19540  mretopd  20706  dvlip  23560  scvxcvx  24512  issubgoilem  27501  cnre2csqlem  29284