Theorem rspc2v 2921

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802

This theorem is referenced by:  rspc2va  2922  rspc3v  2924  disji2  4078  ontriexmidim  4618  wetriext  4673  f1veqaeq  5905  isorel  5944  oveqrspc2v  6040  fovcld  6121  caovclg  6170  caovcomg  6173  smoel  6461  dcdifsnid  6667  unfiexmid  7103  prfidceq  7113  fiintim  7116  supmoti  7183  supsnti  7195  isotilem  7196  onntri35  7445  onntri45  7449  cauappcvgprlem1  7869  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprprlemval  7898  ltordlem  8652  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgrclt  10667  seq3caopr3  10743  seq3homo  10779  seqhomog  10782  climcn2  11860  fprodcl2lem  12156  ennnfonelemim  13035  mhmlin  13540  issubg2m  13766  nsgbi  13781  ghmlin  13825  issubrng2  14214  issubrg2  14245  lmodlema  14296  islmodd  14297  rmodislmodlem  14354  rmodislmod  14355  rnglidlmcl  14484  inopn  14717  basis1  14761  basis2  14762  xmeteq0  15073  cncfi  15292  limccnp2lem  15390  logltb  15588  2sqlem8  15842  redcwlpo  16595  redc0  16597  reap0  16598