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  11591  fprodcl2lem  11887  ennnfonelemim  12766  mhmlin  13270  issubg2m  13496  nsgbi  13511  ghmlin  13555  issubrng2  13943  issubrg2  13974  lmodlema  14025  islmodd  14026  rmodislmodlem  14083  rmodislmod  14084  rnglidlmcl  14213  inopn  14446  basis1  14490  basis2  14491  xmeteq0  14802  cncfi  15021  limccnp2lem  15119  logltb  15317  2sqlem8  15571  redcwlpo  15956  redc0  15958  reap0  15959