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  3727  2reu5lem3  3754  ra4v  3880  rmo3  3884  dftr5  5270  dftr5OLD  5271  reusv3  5404  tfinds2  7853  tfinds3  7854  fpr3g  8270  wfr3g  8307  tfrlem1  8376  tfr3  8399  oeordi  8587  naddssim  8684  ordiso2  9510  ordtypelem7  9519  cantnf  9688  dfac12lem3  10140  ttukeylem5  10508  ttukeylem6  10509  fpwwe2lem7  10632  grudomon  10812  raluz2  12881  bpolycl  15996  ndvdssub  16352  gcdcllem1  16440  acsfn2  17607  pgpfac1  19950  pgpfac  19954  isdomn2  20915  isdomn5  20917  islindf4  21393  isclo2  22592  1stccn  22967  kgencn  23060  txflf  23510  fclsopn  23518  conway  27300  nn0min  32026  bnj580  33924  bnj852  33932  rdgprc  34766  filnetlem4  35266  poimirlem29  36517  heicant  36523  ntrneixb  42846  2rexrsb  45810  tfis2d  47725