rspc2v - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > rspc2v		GIF version

Theorem rspc2v 2961

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)

**Hypotheses**
Ref	Expression
rspc2v.1	⊢ (x = A → (φ ↔ χ))
rspc2v.2	⊢ (y = B → (χ ↔ ψ))

**Assertion**
Ref	Expression
rspc2v	⊢ ((A ∈ C ∧ B ∈ D) → (∀x ∈ C ∀y ∈ D φ → ψ))

Distinct variable groups: x,y,A y,B x,C x,D,y χ,x ψ,y Allowed substitution hints: φ(x,y) ψ(x) χ(y) B(x) C(y)

**Proof of Theorem rspc2v**
Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxχ
2		nfv 1619	. 2 ⊢ Ⅎyψ
3		rspc2v.1	. 2 ⊢ (x = A → (φ ↔ χ))
4		rspc2v.2	. 2 ⊢ (y = B → (χ ↔ ψ))
5	1, 2, 3, 4	rspc2 2960	1 ⊢ ((A ∈ C ∧ B ∈ D) → (∀x ∈ C ∀y ∈ D φ → ψ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 176 ∧ wa 358 = wceq 1642 ∈ wcel 1710 ∀wral 2614

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ral 2619 df-v 2861

This theorem is referenced by: rspc2va 2962 rspc3v 2964 ncfinraise 4481 nnpweq 4523 isorel 5489 isotr 5495 fovcl 5588 caovcld 5622 caovcomg 5624 extd 5923 symd 5924 antid 5929 connexd 5931