Theorem rspc2va 3621

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  rspc2dv  3624  swopo  5597  soisores  7318  soisoi  7319  isocnv  7321  isotr  7327  ovrspc2v  7429  caofrss  7700  caonncan  7705  frpoins3xpg  8120  coflton  8665  wunpr  10699  injresinj  13748  seqcaopr2  13999  rlimcn3  15529  o1of2  15552  isprm6  16646  ssc2  17764  pospropd  18275  tleile  18369  mhmpropd  18673  grpidssd  18894  grpinvssd  18895  dfgrp3lem  18916  isnsg3  19033  cyccom  19073  symgextf1  19281  efgredlemd  19604  efgredlem  19607  rglcom4d  20024  issrngd  20456  domneq0  20899  lindfind  21354  lindsind  21355  mplsubglem  21539  mdetunilem1  22095  mdetunilem3  22097  mdetunilem4  22098  mdetunilem9  22103  decpmatmulsumfsupp  22256  pm2mpf1  22282  pm2mpmhmlem1  22301  t0sep  22809  tsmsxplem2  23639  comet  24003  nrmmetd  24064  tngngp  24152  reconnlem2  24324  iscmet3lem1  24789  iscmet3lem2  24790  dchrisumlem1  26971  pntpbnd1  27068  ssltsepc  27273  tgjustc1  27705  tgjustc2  27706  iscgrglt  27744  motcgr  27766  perpneq  27944  foot  27952  f1otrg  28101  axcontlem10  28210  frgr2wwlk1  29561  orngmul  32389  lindsunlem  32653  mndpluscn  32843  unelros  33106  difelros  33107  inelsros  33113  diffiunisros  33114  cvxsconn  34171  elmrsubrn  34448  ghomco  36696  sticksstones10  40908  sticksstones12a  40910  fsuppind  41111  mzpcl34  41401  ntrk0kbimka  42722  isotone1  42731  isotone2  42732  nnfoctbdjlem  45105  isomuspgrlem2d  46433  mgmhmpropd  46489  rnghmmul  46631  2arymaptf1  47240