Theorem rspc2v 2889

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 1550	. 2 ⊢ Ⅎ𝑥𝜒
2		nfv 1550	. 2 ⊢ Ⅎ𝑦𝜓
3		rspc2v.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
4		rspc2v.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	1, 2, 3, 4	rspc2 2887	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1372   ∈ wcel 2175  ∀wral 2483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773

This theorem is referenced by:  rspc2va  2890  rspc3v  2892  disji2  4036  ontriexmidim  4569  wetriext  4624  f1veqaeq  5837  isorel  5876  oveqrspc2v  5970  fovcld  6049  caovclg  6098  caovcomg  6101  smoel  6385  dcdifsnid  6589  unfiexmid  7014  prfidceq  7024  fiintim  7027  supmoti  7094  supsnti  7106  isotilem  7107  onntri35  7348  onntri45  7352  cauappcvgprlem1  7771  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprprlemval  7800  ltordlem  8554  frecuzrdgrrn  10551  frec2uzrdg  10552  frecuzrdgrcl  10553  frecuzrdgrclt  10558  seq3caopr3  10634  seq3homo  10670  seqhomog  10673  climcn2  11562  fprodcl2lem  11858  ennnfonelemim  12737  mhmlin  13241  issubg2m  13467  nsgbi  13482  ghmlin  13526  issubrng2  13914  issubrg2  13945  lmodlema  13996  islmodd  13997  rmodislmodlem  14054  rmodislmod  14055  rnglidlmcl  14184  inopn  14417  basis1  14461  basis2  14462  xmeteq0  14773  cncfi  14992  limccnp2lem  15090  logltb  15288  2sqlem8  15542  redcwlpo  15927  redc0  15929  reap0  15930