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 1931. (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 389 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) | |
2 | 1 | albii 1811 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) |
3 | 19.21v 1931 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) | |
4 | 2, 3 | bitri 276 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
5 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) | |
6 | df-ral 3143 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
7 | 6 | imbi2i 337 | . 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
8 | 4, 5, 7 | 3bitr4i 304 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 ∈ wcel 2105 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-ral 3143 |
This theorem is referenced by: r19.23v 3279 r19.32v 3340 rmo4 3720 2reu5lem3 3747 ra4v 3867 rmo3 3871 rmo3OLD 3872 dftr5 5167 reusv3 5297 tfinds2 7566 tfinds3 7567 wfr3g 7944 tfrlem1 8003 tfr3 8026 oeordi 8203 ordiso2 8968 ordtypelem7 8977 cantnf 9145 dfac12lem3 9560 ttukeylem5 9924 ttukeylem6 9925 fpwwe2lem8 10048 grudomon 10228 raluz2 12286 bpolycl 15396 ndvdssub 15750 gcdcllem1 15838 acsfn2 16924 pgpfac1 19133 pgpfac 19137 isdomn2 20002 islindf4 20912 isclo2 21626 1stccn 22001 kgencn 22094 txflf 22544 fclsopn 22552 nn0min 30464 bnj580 32085 bnj852 32093 rdgprc 32937 fpr3g 33020 conway 33162 filnetlem4 33627 poimirlem29 34803 heicant 34809 ntrneixb 40325 2rexrsb 43181 tfis2d 44681 |
Copyright terms: Public domain | W3C validator |