Theorem vtocl2g 3533

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2178, ax-11 2194, and ax-13 2401. (Revised by Steven Nguyen, 29-Nov-2022.)

Hypotheses

Ref	Expression
vtocl2g.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtocl2g.2	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
vtocl2g.3	⊢ 𝜑

Assertion

Ref	Expression
vtocl2g	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

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

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

Proof of Theorem vtocl2g

Step	Hyp	Ref	Expression
1		elex 3471	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		vtocl2g.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
3	2	imbi2d 343	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4		vtocl2g.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5		vtocl2g.3	. . . 4 ⊢ 𝜑
6	4, 5	vtoclg 3517	. . 3 ⊢ (𝐴 ∈ V → 𝜓)
7	3, 6	vtoclg 3517	. 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒))
8	1, 7	mpan9 516	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  vtocl3g  3534  vtocl4g  3541  opthg  5453  opelopabsb  5508  vtoclr  5718  funopg  6568  f1osng  6861  fsng  7132  fnpr2g  7210  op1stg  7999  op2ndg  8000  xpsneng  9063  xpcomeng  9070  sbth  9098  sbthfi  9196  unxpdom  9232  prcdnq  11005  mhmlem  19188  carsgmon  34828  brimageg  36507  brdomaing  36515  brrangeg  36516  rankung  36749  mbfresfi  38418  zindbi  43790  2sbc6g  45242  2sbc5g  45243  fmulcl  46414