Theorem r19.21v 3180

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  r19.23v  3183  r19.32v  3192  cbvraldva  3239  rmo4  3736  2reu5lem3  3763  ra4v  3885  rmo3  3889  dftr5  5263  dftr5OLD  5264  reusv3  5405  tfinds2  7885  tfinds3  7886  fpr3g  8310  wfr3g  8347  tfrlem1  8416  tfr3  8439  oeordi  8625  naddssim  8723  ordiso2  9555  ordtypelem7  9564  cantnf  9733  dfac12lem3  10186  ttukeylem5  10553  ttukeylem6  10554  fpwwe2lem7  10677  grudomon  10857  raluz2  12939  bpolycl  16088  ndvdssub  16446  gcdcllem1  16536  acsfn2  17706  pgpfac1  20100  pgpfac  20104  isdomn5  20710  isdomn2OLD  20712  islindf4  21858  isclo2  23096  1stccn  23471  kgencn  23564  txflf  24014  fclsopn  24022  conway  27844  nn0min  32822  bnj580  34927  bnj852  34935  rdgprc  35795  filnetlem4  36382  poimirlem29  37656  heicant  37662  indstrd  42194  ntrneixb  44108  trfr  44979  modelac8prim  45009  2rexrsb  47114  tfis2d  49199