Theorem vtocl2ga 3402

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 2890	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2890	. 2 ⊢ Ⅎ𝑦𝐴
3		nfcv 2890	. 2 ⊢ Ⅎ𝑦𝐵
4		nfv 1980	. 2 ⊢ Ⅎ𝑥𝜓
5		nfv 1980	. 2 ⊢ Ⅎ𝑦𝜒
6		vtocl2ga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7		vtocl2ga.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
8		vtocl2ga.3	. 2 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)
9	1, 2, 3, 4, 5, 6, 7, 8	vtocl2gaf 3401	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1620   ∈ wcel 2127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330

This theorem is referenced by:  solin  5198  caovcan  6991  pwfseqlem2  9644  mulcanenq  9945  ltaddnq  9959  ltrnq  9964  genpv  9984  wrdind  13647  fsumrelem  14709  imasleval  16374  fullfunc  16738  fthfunc  16739  pf1ind  19892  mretopd  21069  dvlip  23926  scvxcvx  24882  issubgoilem  28397  cnre2csqlem  30236