Theorem rspc2va 3633

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2va	⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2va

Step	Hyp	Ref	Expression
1		rspc2v.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
3	1, 2	rspc2v 3632	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 409	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143

This theorem is referenced by:  swopo  5483  soisores  7079  soisoi  7080  isocnv  7082  isotr  7088  ovrspc2v  7181  caofrss  7441  caonncan  7446  wunpr  10130  injresinj  13157  seqcaopr2  13405  rlimcn2  14946  o1of2  14968  isprm6  16057  ssc2  17091  pospropd  17743  mhmpropd  17961  grpidssd  18174  grpinvssd  18175  dfgrp3lem  18196  isnsg3  18311  cyccom  18345  symgextf1  18548  efgredlemd  18869  efgredlem  18872  issrngd  19631  domneq0  20069  mplsubglem  20213  lindfind  20959  lindsind  20960  mdetunilem1  21220  mdetunilem3  21222  mdetunilem4  21223  mdetunilem9  21228  decpmatmulsumfsupp  21380  pm2mpf1  21406  pm2mpmhmlem1  21425  t0sep  21931  tsmsxplem2  22761  comet  23122  nrmmetd  23183  tngngp  23262  reconnlem2  23434  iscmet3lem1  23893  iscmet3lem2  23894  dchrisumlem1  26064  pntpbnd1  26161  tgjustc1  26260  tgjustc2  26261  iscgrglt  26299  motcgr  26321  perpneq  26499  foot  26507  f1otrg  26656  axcontlem10  26758  frgr2wwlk1  28107  tleile  30648  orngmul  30876  lindsunlem  31020  mndpluscn  31169  unelros  31430  difelros  31431  inelsros  31437  diffiunisros  31438  cvxsconn  32490  elmrsubrn  32767  ghomco  35168  mzpcl34  39326  ntrk0kbimka  40387  isotone1  40396  isotone2  40397  nnfoctbdjlem  42736  isomuspgrlem2d  43995  mgmhmpropd  44051  rnghmmul  44170