Theorem rspc2v 2937

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2205  ∀wral 2522

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817

This theorem is referenced by:  rspc2va  2938  rspc3v  2940  disji2  4106  ontriexmidim  4649  wetriext  4704  f1veqaeq  5948  isorel  5987  oveqrspc2v  6085  fovcld  6166  caovclg  6215  caovcomg  6218  smoel  6544  dcdifsnid  6750  unfiexmid  7191  prfidceq  7201  fiintim  7204  supmoti  7297  supsnti  7309  isotilem  7310  onntri35  7560  onntri45  7564  cauappcvgprlem1  7990  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprprlemval  8019  ltordlem  8773  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgrclt  10801  seq3caopr3  10877  seq3homo  10913  seqhomog  10916  climcn2  12019  fprodcl2lem  12316  ennnfonelemim  13259  mhmlin  13722  issubg2m  13942  nsgbi  13957  ghmlin  14001  issubrng2  14456  issubrg2  14487  lmodlema  14566  islmodd  14567  rmodislmodlem  14624  rmodislmod  14625  rnglidlmcl  14754  inopn  14994  basis1  15038  basis2  15039  xmeteq0  15350  cncfi  15569  limccnp2lem  15667  logltb  15865  2sqlem8  16122  redcwlpo  16966  redc0  16968  reap0  16969