Theorem r19.21v 3163

Description: Restricted quantifier version of 19.21v 1941. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 11-Dec-2024.)

Assertion

Ref	Expression
r19.21v	⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem r19.21v

Step	Hyp	Ref	Expression
1		pm2.27 42	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	ralimdv 3152	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3134	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  r19.23v  3165  r19.32v  3171  cbvraldva  3218  rmo4  3677  2reu5lem3  3704  ra4v  3824  rmo3  3828  dftr5  5197  reusv3  5343  tfinds2  7809  tfinds3  7810  fpr3g  8229  wfr3g  8263  tfrlem1  8309  tfr3  8332  oeordi  8517  naddssim  8615  ordiso2  9424  ordtypelem7  9433  cantnf  9608  dfac12lem3  10062  ttukeylem5  10429  ttukeylem6  10430  fpwwe2lem7  10554  grudomon  10734  raluz2  12841  bpolycl  16011  ndvdssub  16372  gcdcllem1  16462  acsfn2  17623  pgpfac1  20051  pgpfac  20055  isdomn5  20681  isdomn2OLD  20683  islindf4  21831  isclo2  23066  1stccn  23441  kgencn  23534  txflf  23984  fclsopn  23992  conway  27788  nn0min  32912  bnj580  35074  bnj852  35082  rdgprc  35993  filnetlem4  36582  poimirlem29  37987  heicant  37993  indstrd  42649  ntrneixb  44543  trfr  45410  modelac8prim  45440  2rexrsb  47565  tfis2d  50170