Theorem rspc 2904

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 2515	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2374	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1576	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1620	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2294	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 234	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 2888	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 51	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 152	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1395   = wceq 1397  Ⅎwnf 1508   ∈ wcel 2202  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  rspcv  2906  rspc2  2921  rspc2vd  3196  pofun  4409  omsinds  4720  fmptcof  5814  fliftfuns  5939  qliftfuns  6788  xpf1o  7030  finexdc  7092  ssfirab  7129  opabfi  7132  iunfidisj  7145  dcfi  7180  cc3  7487  lble  9127  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  uzsinds  10707  sumeq2  11924  sumfct  11939  sumrbdclem  11943  summodclem3  11946  summodclem2a  11947  zsumdc  11950  fsumgcl  11952  fsum3  11953  fsumf1o  11956  isumss  11957  isumss2  11959  fsum3cvg2  11960  fsumadd  11972  isummulc2  11992  fsum2dlemstep  12000  fisumcom2  12004  fsumshftm  12011  fisum0diag2  12013  fsummulc2  12014  fsum00  12028  fsumabs  12031  fsumrelem  12037  fsumiun  12043  isumshft  12056  mertenslem2  12102  prodeq2  12123  prodrbdclem  12137  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  prodfct  12153  fprodf1o  12154  prodssdc  12155  fprodmul  12157  fprodm1s  12167  fprodp1s  12168  fprodabs  12182  fprodap0  12187  fprod2dlemstep  12188  fprodcom2fi  12192  fprodrec  12195  fprodap0f  12202  fprodle  12206  bezoutlemmain  12574  nnwosdc  12615  pcmpt  12921  ctiunctlemudc  13063  gsumfzfsumlemm  14607  iuncld  14845  txcnp  15001  fsumcncntop  15297  bj-nntrans  16572