Theorem r19.21v 3173

Description: Restricted quantifier version of 19.21v 1942. (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 3163	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3144	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wral 3062

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 1913

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  r19.23v  3176  r19.32v  3185  rmo4  3679  2reu5lem3  3706  ra4v  3832  rmo3  3836  dftr5  5217  dftr5OLD  5218  reusv3  5352  tfinds2  7782  tfinds3  7783  fpr3g  8175  wfr3g  8212  tfrlem1  8281  tfr3  8304  oeordi  8493  ordiso2  9376  ordtypelem7  9385  cantnf  9554  dfac12lem3  10006  ttukeylem5  10374  ttukeylem6  10375  fpwwe2lem7  10498  grudomon  10678  raluz2  12742  bpolycl  15861  ndvdssub  16217  gcdcllem1  16305  acsfn2  17469  pgpfac1  19777  pgpfac  19781  isdomn2  20675  islindf4  21150  isclo2  22344  1stccn  22719  kgencn  22812  txflf  23262  fclsopn  23270  conway  27043  nn0min  31419  bnj580  33190  bnj852  33198  rdgprc  34053  naddssim  34122  filnetlem4  34707  poimirlem29  35962  heicant  35968  isdomn5  40479  ntrneixb  42078  2rexrsb  45012  tfis2d  46804