Theorem rspc 3303

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)

Hypotheses

Ref	Expression
rspc.1	⊢ Ⅎ𝑥𝜓
rspc.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspc	⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspc

Step	Hyp	Ref	Expression
1		df-ral 2917	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2764	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1843	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1825	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2689	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 334	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3288	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	syl5bi 232	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481   = wceq 1483  Ⅎwnf 1708   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  rspcv  3305  rspc2  3320  disjxiun  4649  disjxiunOLD  4650  pofun  5051  fmptcof  6397  fliftfuns  6564  ofmpteq  6916  qliftfuns  7834  xpf1o  8122  iunfi  8254  iundom2g  9362  lble  10975  rlimcld2  14309  sumeq2ii  14423  summolem3  14445  zsum  14449  fsum  14451  fsumf1o  14454  sumss2  14457  fsumcvg2  14458  fsumadd  14470  isummulc2  14493  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsum0diag2  14515  fsummulc2  14516  fsum00  14530  fsumabs  14533  fsumrelem  14539  fsumrlim  14543  fsumo1  14544  o1fsum  14545  fsumiun  14553  isumshft  14571  prodeq2ii  14643  prodmolem3  14663  zprod  14667  fprod  14671  fprodf1o  14676  prodss  14677  fprodser  14679  fprodmul  14690  fproddiv  14691  fprodm1s  14700  fprodp1s  14701  fprodabs  14704  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  fprodefsum  14825  sumeven  15110  sumodd  15111  pcmpt  15596  invfuc  16634  dprd2d2  18443  txcnp  21423  ptcnplem  21424  prdsdsf  22172  prdsxmet  22174  fsumcn  22673  ovolfiniun  23269  ovoliunnul  23275  volfiniun  23315  iunmbl  23321  limciun  23658  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlim  23794  dvfsumrlim2  23795  dvfsum2  23797  itgsubst  23812  fsumvma  24938  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  rspc2vd  27129  chirred  29254  fsumiunle  29575  sigapildsyslem  30224  voliune  30292  volfiniune  30293  tfisg  31716  nosupbnd1  31860  ptrest  33408  poimirlem25  33434  poimirlem26  33435  mzpsubst  37311  rabdiophlem2  37366  etransclem48  40499  sge0iunmpt  40635