Theorem rspc2va 3647

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  rspc2dv  3650  swopo  5619  soisores  7363  soisoi  7364  isocnv  7366  isotr  7372  ovrspc2v  7474  coof  7737  caofrss  7751  caonncan  7756  frpoins3xpg  8181  coflton  8727  wunpr  10778  injresinj  13838  seqcaopr2  14089  rlimcn3  15636  o1of2  15659  isprm6  16761  ssc2  17883  pospropd  18397  tleile  18491  mgmhmpropd  18736  mhmpropd  18827  grpidssd  19056  grpinvssd  19057  dfgrp3lem  19078  isnsg3  19200  cyccom  19243  symgextf1  19463  efgredlemd  19786  efgredlem  19789  rglcom4d  20238  rnghmmul  20475  domneq0  20730  issrngd  20878  lindfind  21859  lindsind  21860  mplsubglem  22042  mdetunilem1  22639  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  decpmatmulsumfsupp  22800  pm2mpf1  22826  pm2mpmhmlem1  22845  t0sep  23353  tsmsxplem2  24183  comet  24547  nrmmetd  24608  tngngp  24696  reconnlem2  24868  iscmet3lem1  25344  iscmet3lem2  25345  dchrisumlem1  27551  pntpbnd1  27648  ssltsepc  27856  tgjustc1  28501  tgjustc2  28502  iscgrglt  28540  motcgr  28562  perpneq  28740  foot  28748  f1otrg  28897  axcontlem10  29006  frgr2wwlk1  30361  orngmul  33298  lindsunlem  33637  mndpluscn  33872  unelros  34135  difelros  34136  inelsros  34142  diffiunisros  34143  elmrsubrn  35488  ghomco  37851  sticksstones10  42112  sticksstones12a  42114  fsuppind  42545  mzpcl34  42687  ntrk0kbimka  44001  isotone1  44010  isotone2  44011  nnfoctbdjlem  46376  2arymaptf1  48387