Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbi | Structured version Visualization version GIF version |
Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1825. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
Ref | Expression |
---|---|
ralbi | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp 218 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | |
2 | 1 | ral2imi 3072 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
3 | biimpr 223 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | |
4 | 3 | ral2imi 3072 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑)) |
5 | 2, 4 | impbid 215 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wral 3054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 |
This theorem depends on definitions: df-bi 210 df-ral 3059 |
This theorem is referenced by: rexbi 3156 uniiunlem 3985 iineq2 4911 reusv2lem5 5279 ralrnmptw 6882 ralrnmpt 6884 f1mpt 7042 mpo2eqb 7310 ralrnmpo 7316 rankonidlem 9342 acni2 9558 kmlem8 9669 kmlem13 9674 fimaxre3 11676 cau3lem 14816 rlim2 14955 rlim0 14967 rlim0lt 14968 catpropd 17095 funcres2b 17284 ulmss 25156 lgamgulmlem6 25783 colinearalg 26868 axpasch 26899 axcontlem2 26923 axcontlem4 26925 axcontlem7 26928 axcontlem8 26929 naddcom 33490 naddid1 33491 neibastop3 34206 bj-0int 34925 ralbi12f 35973 iineq12f 35977 pmapglbx 37438 ordelordALTVD 42065 |
Copyright terms: Public domain | W3C validator |