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 1936. (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.) |
Ref | Expression |
---|---|
r19.21v | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi2.04 391 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) | |
2 | 1 | albii 1816 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) |
3 | 19.21v 1936 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) | |
4 | 2, 3 | bitri 277 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
5 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) | |
6 | df-ral 3143 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
7 | 6 | imbi2i 338 | . 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
8 | 4, 5, 7 | 3bitr4i 305 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1531 ∈ wcel 2110 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 |
This theorem depends on definitions: df-bi 209 df-ex 1777 df-ral 3143 |
This theorem is referenced by: r19.23v 3279 r19.32v 3340 rmo4 3721 2reu5lem3 3748 ra4v 3868 rmo3 3872 rmo3OLD 3873 dftr5 5168 reusv3 5298 tfinds2 7572 tfinds3 7573 wfr3g 7947 tfrlem1 8006 tfr3 8029 oeordi 8207 ordiso2 8973 ordtypelem7 8982 cantnf 9150 dfac12lem3 9565 ttukeylem5 9929 ttukeylem6 9930 fpwwe2lem8 10053 grudomon 10233 raluz2 12291 bpolycl 15400 ndvdssub 15754 gcdcllem1 15842 acsfn2 16928 pgpfac1 19196 pgpfac 19200 isdomn2 20066 islindf4 20976 isclo2 21690 1stccn 22065 kgencn 22158 txflf 22608 fclsopn 22616 nn0min 30531 bnj580 32180 bnj852 32188 rdgprc 33034 fpr3g 33117 conway 33259 filnetlem4 33724 poimirlem29 34915 heicant 34921 ntrneixb 40438 2rexrsb 43293 tfis2d 44776 |
Copyright terms: Public domain | W3C validator |