| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > r19.21v | Structured version Visualization version GIF version | ||
| Description: Restricted quantifier version of 19.21v 1972. (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.) |
| Ref | Expression |
|---|---|
| r19.21v | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.27 43 | . . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) | |
| 2 | 1 | ralimdv 3181 | . . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)) |
| 3 | 2 | com12 33 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
| 4 | pm2.21 124 | . . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
| 5 | 4 | ralrimivw 3163 | . . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
| 6 | ax-1 6 | . . . 4 ⊢ (𝜓 → (𝜑 → 𝜓)) | |
| 7 | 6 | ralimi 3104 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
| 8 | 5, 7 | ja 188 | . 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
| 9 | 3, 8 | impbii 212 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∀wral 3081 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 |
| This proof depends on definitions: df-bi 210 df-an 402 df-ral 3082 |
| This theorem is used by: r19.23v 3194 r19.32v 3200 cbvraldva 3247 rmo4 3695 2reu5lem3 3722 ra4v 3839 rmo3 3843 dftr5 5224 reusv3 5378 tfinds2 7866 tfinds3 7867 fpr3g 8288 wfr3g 8322 tfrlem1 8368 tfr3 8392 oeordi 8579 naddssim 8678 ordiso2 9484 ordtypelem7 9493 cantnf 9669 dfac12lem3 10145 ttukeylem5 10512 ttukeylem6 10513 fpwwe2lem7 10637 grudomon 10817 raluz2 12937 bpolycl 16128 ndvdssub 16489 gcdcllem1 16579 acsfn2 17741 pgpfac1 20196 pgpfac 20200 isdomn5 20859 islindf4 22038 isclo2 23295 1stccn 23671 kgencn 23764 txflf 24214 fclsopn 24222 conway 28023 nn0min 33235 bnj580 35366 bnj852 35374 rdgprc 36321 filnetlem4 36949 poimirlem29 38357 heicant 38363 indstrd 43018 ntrneixb 44879 trfr 45729 modelac8prim 45759 2rexrsb 47897 tfis2d 50515 |
| Copyright terms: Public domain | W3C validator |