Theorem rspc2v 2843

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

Hypotheses

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

Assertion

Ref	Expression
rspc2v	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

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

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

Proof of Theorem rspc2v

Step	Hyp	Ref	Expression
1		nfv 1516	. 2 ⊢ Ⅎ𝑥𝜒
2		nfv 1516	. 2 ⊢ Ⅎ𝑦𝜓
3		rspc2v.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
4		rspc2v.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	1, 2, 3, 4	rspc2 2841	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1343   ∈ wcel 2136  ∀wral 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-v 2728

This theorem is referenced by:  rspc2va  2844  rspc3v  2846  disji2  3975  ontriexmidim  4499  wetriext  4554  f1veqaeq  5737  isorel  5776  oveqrspc2v  5869  fovcl  5947  caovclg  5994  caovcomg  5997  smoel  6268  dcdifsnid  6472  unfiexmid  6883  fiintim  6894  supmoti  6958  supsnti  6970  isotilem  6971  onntri35  7193  onntri45  7197  cauappcvgprlem1  7600  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprprlemval  7629  ltordlem  8380  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgrclt  10350  seq3caopr3  10416  seq3homo  10445  climcn2  11250  fprodcl2lem  11546  ennnfonelemim  12357  inopn  12641  basis1  12685  basis2  12686  xmeteq0  12999  cncfi  13205  limccnp2lem  13285  logltb  13435  2sqlem8  13599  redcwlpo  13934  redc0  13936  reap0  13937