Theorem r19.21v 3180

Description: Restricted quantifier version of 19.21v 1943. (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 3170	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3151	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3084	. . 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 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  r19.23v  3183  r19.32v  3192  cbvraldva  3237  rmo4  3726  2reu5lem3  3753  ra4v  3879  rmo3  3883  dftr5  5269  dftr5OLD  5270  reusv3  5403  tfinds2  7850  tfinds3  7851  fpr3g  8267  wfr3g  8304  tfrlem1  8373  tfr3  8396  oeordi  8584  naddssim  8681  ordiso2  9507  ordtypelem7  9516  cantnf  9685  dfac12lem3  10137  ttukeylem5  10505  ttukeylem6  10506  fpwwe2lem7  10629  grudomon  10809  raluz2  12878  bpolycl  15993  ndvdssub  16349  gcdcllem1  16437  acsfn2  17604  pgpfac1  19945  pgpfac  19949  isdomn2  20908  isdomn5  20910  islindf4  21385  isclo2  22584  1stccn  22959  kgencn  23052  txflf  23502  fclsopn  23510  conway  27290  nn0min  32014  bnj580  33913  bnj852  33921  rdgprc  34755  filnetlem4  35255  poimirlem29  36506  heicant  36512  ntrneixb  42832  2rexrsb  45797  tfis2d  47679