Theorem r19.21v 3186

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  r19.23v  3189  r19.32v  3198  cbvraldva  3245  rmo4  3752  2reu5lem3  3779  ra4v  3907  rmo3  3911  dftr5  5287  dftr5OLD  5288  reusv3  5423  tfinds2  7901  tfinds3  7902  fpr3g  8326  wfr3g  8363  tfrlem1  8432  tfr3  8455  oeordi  8643  naddssim  8741  ordiso2  9584  ordtypelem7  9593  cantnf  9762  dfac12lem3  10215  ttukeylem5  10582  ttukeylem6  10583  fpwwe2lem7  10706  grudomon  10886  raluz2  12962  bpolycl  16100  ndvdssub  16457  gcdcllem1  16545  acsfn2  17721  pgpfac1  20124  pgpfac  20128  isdomn5  20732  isdomn2OLD  20734  islindf4  21881  isclo2  23117  1stccn  23492  kgencn  23585  txflf  24035  fclsopn  24043  conway  27862  nn0min  32824  bnj580  34889  bnj852  34897  rdgprc  35758  filnetlem4  36347  poimirlem29  37609  heicant  37615  indstrd  42150  ntrneixb  44057  2rexrsb  47017  tfis2d  48772