Theorem rspc2dv 3590

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 3587	. 2 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜓) → 𝜒)
7	1, 2, 3, 6	syl21anc 851	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  prmidlprop  21633  mulscom  28526  addsdilem3  28540  addsdilem4  28541  mulsasslem3  28552  rprmdvds  34094  mplvrpmga  34220  vieta  34255  cvxsconn  36077  nmulprop  37014  nmulcom  37018  nadddilem1  37044  nadddilem3  37046  oppcmndclem  50201  ssccatid  50256  termcbasmo  50667  fulltermc2  50696  arweuthinc  50713  arweutermc  50714