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 1855. (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 375 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) | |
2 | 1 | albii 1737 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) |
3 | 19.21v 1855 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) | |
4 | 2, 3 | bitri 263 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
5 | df-ral 2901 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) | |
6 | df-ral 2901 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
7 | 6 | imbi2i 325 | . 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
8 | 4, 5, 7 | 3bitr4i 291 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-ex 1696 df-ral 2901 |
This theorem is referenced by: r19.23v 3005 r19.32v 3064 rmo4 3366 2reu5lem3 3382 ra4v 3490 rmo3 3494 dftr5 4683 reusv3 4802 tfinds2 6955 tfinds3 6956 wfr3g 7300 tfrlem1 7359 tfr3 7382 oeordi 7554 ordiso2 8303 ordtypelem7 8312 cantnf 8473 dfac12lem3 8850 ttukeylem5 9218 ttukeylem6 9219 fpwwe2lem8 9338 grudomon 9518 raluz2 11613 bpolycl 14622 ndvdssub 14971 gcdcllem1 15059 acsfn2 16147 pgpfac1 18302 pgpfac 18306 isdomn2 19120 islindf4 19996 isclo2 20702 1stccn 21076 kgencn 21169 txflf 21620 fclsopn 21628 nn0min 28954 bnj580 30237 bnj852 30245 rdgprc 30944 filnetlem4 31546 poimirlem29 32608 heicant 32614 ntrneixb 37413 2rexrsb 39820 tfis2d 42225 |
Copyright terms: Public domain | W3C validator |