Theorem rspc2va 3577

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 3576	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 406	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rspc2dv  3580  swopo  5544  f1ounsn  7221  soisores  7276  soisoi  7277  isocnv  7279  isotr  7285  ovrspc2v  7387  coof  7649  caofrss  7664  caonncan  7669  frpoins3xpg  8084  coflton  8601  wunpr  10626  injresinj  13740  seqcaopr2  13994  rlimcn3  15546  o1of2  15569  isprm6  16678  ssc2  17783  pospropd  18285  tleile  18379  mgmhmpropd  18660  mhmpropd  18754  grpidssd  18986  grpinvssd  18987  dfgrp3lem  19008  isnsg3  19129  cyccom  19172  symgextf1  19390  efgredlemd  19713  efgredlem  19716  rglcom4d  20186  rnghmmul  20423  domneq0  20679  issrngd  20826  orngmul  20836  lindfind  21809  lindsind  21810  mplsubglem  21990  mdetunilem1  22590  mdetunilem3  22592  mdetunilem4  22593  mdetunilem9  22598  decpmatmulsumfsupp  22751  pm2mpf1  22777  pm2mpmhmlem1  22796  t0sep  23302  tsmsxplem2  24132  comet  24491  nrmmetd  24552  tngngp  24632  reconnlem2  24806  iscmet3lem1  25271  iscmet3lem2  25272  dchrisumlem1  27469  pntpbnd1  27566  sltssepc  27780  tgjustc1  28560  tgjustc2  28561  iscgrglt  28599  motcgr  28621  perpneq  28799  foot  28807  f1otrg  28956  axcontlem10  29059  frgr2wwlk1  30417  lindsunlem  33787  mndpluscn  34089  unelros  34334  difelros  34335  inelsros  34341  diffiunisros  34342  elmrsubrn  35721  ghomco  38229  sticksstones10  42611  sticksstones12a  42613  fsuppind  43040  mzpcl34  43180  ntrk0kbimka  44487  isotone1  44496  isotone2  44497  nnfoctbdjlem  46904  2arymaptf1  49144