Theorem rspc2dv 3605

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 6-Mar-2025.)

Hypotheses

Ref	Expression
rspc2dv.1	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
rspc2dv.2	⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜒))
rspc2dv.3	⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜓)
rspc2dv.4	⊢ (𝜑 → 𝐴 ∈ 𝐶)
rspc2dv.5	⊢ (𝜑 → 𝐵 ∈ 𝐷)

Assertion

Ref	Expression
rspc2dv	⊢ (𝜑 → 𝜒)

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

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

Proof of Theorem rspc2dv

Step	Hyp	Ref	Expression
1		rspc2dv.4	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
2		rspc2dv.5	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷)
3		rspc2dv.3	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜓)
4		rspc2dv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
5		rspc2dv.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜒))
6	4, 5	rspc2va 3602	. 2 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜓) → 𝜒)
7	1, 2, 3, 6	syl21anc 850	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  prmidlprop  21445  mulscom  28298  addsdilem3  28312  addsdilem4  28313  mulsasslem3  28324  rprmdvds  33754  mplvrpmga  33880  vieta  33915  cvxsconn  35634  nmulprop  36581  nmulcom  36585  oppcmndclem  49680  ssccatid  49735  termcbasmo  50146  fulltermc2  50175  arweuthinc  50192  arweutermc  50193