Theorem rspc2v 2920

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 2918	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 2801

This theorem is referenced by:  rspc2va  2921  rspc3v  2923  disji2  4074  ontriexmidim  4613  wetriext  4668  f1veqaeq  5892  isorel  5931  oveqrspc2v  6027  fovcld  6108  caovclg  6157  caovcomg  6160  smoel  6444  dcdifsnid  6648  unfiexmid  7076  prfidceq  7086  fiintim  7089  supmoti  7156  supsnti  7168  isotilem  7169  onntri35  7418  onntri45  7422  cauappcvgprlem1  7842  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprprlemval  7871  ltordlem  8625  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgrclt  10632  seq3caopr3  10708  seq3homo  10744  seqhomog  10747  climcn2  11815  fprodcl2lem  12111  ennnfonelemim  12990  mhmlin  13495  issubg2m  13721  nsgbi  13736  ghmlin  13780  issubrng2  14168  issubrg2  14199  lmodlema  14250  islmodd  14251  rmodislmodlem  14308  rmodislmod  14309  rnglidlmcl  14438  inopn  14671  basis1  14715  basis2  14716  xmeteq0  15027  cncfi  15246  limccnp2lem  15344  logltb  15542  2sqlem8  15796  redcwlpo  16382  redc0  16384  reap0  16385