This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspc2vd

Description: Deduction version of 2-variable restricted specialization, using implicit substitution. Notice that the class D for the second set variable y may depend on the first set variable x . (Contributed by AV, 29-Mar-2021)

		Ref	Expression
	Hypotheses	rspc2vd.a	⊢ ( 𝑥 = 𝐴 → ( 𝜃 ↔ 𝜒 ) )
		rspc2vd.b	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
		rspc2vd.c	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
		rspc2vd.d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐷 = 𝐸 )
		rspc2vd.e	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
	Assertion	rspc2vd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜃 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rspc2vd.a	⊢ ( 𝑥 = 𝐴 → ( 𝜃 ↔ 𝜒 ) )
2		rspc2vd.b	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
3		rspc2vd.c	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
4		rspc2vd.d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐷 = 𝐸 )
5		rspc2vd.e	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
6	3 4	csbied	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = 𝐸 )
7	5 6	eleqtrrd	⊢ ( 𝜑 → 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 )
8		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐷
9		nfv	⊢ Ⅎ 𝑥 𝜒
10	8 9	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 𝜒
11		csbeq1a	⊢ ( 𝑥 = 𝐴 → 𝐷 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 )
12	11 1	raleqbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝐷 𝜃 ↔ ∀ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 𝜒 ) )
13	10 12	rspc	⊢ ( 𝐴 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜃 → ∀ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 𝜒 ) )
14	3 13	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜃 → ∀ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 𝜒 ) )
15	2	rspcv	⊢ ( 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 → ( ∀ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 𝜒 → 𝜓 ) )
16	7 14 15	sylsyld	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜃 → 𝜓 ) )