![]() |
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 1800. (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 216 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | |
2 | 1 | ral2imi 3123 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
3 | biimpr 221 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | |
4 | 3 | ral2imi 3123 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑)) |
5 | 2, 4 | impbid 213 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wral 3105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 |
This theorem depends on definitions: df-bi 208 df-ral 3110 |
This theorem is referenced by: uniiunlem 3982 iineq2 4844 reusv2lem5 5194 ralrnmpt 6725 f1mpt 6884 mpo2eqb 7139 ralrnmpo 7145 rankonidlem 9103 acni2 9318 kmlem8 9429 kmlem13 9434 fimaxre3 11435 cau3lem 14548 rlim2 14687 rlim0 14699 rlim0lt 14700 catpropd 16808 funcres2b 16996 ulmss 24668 lgamgulmlem6 25293 colinearalg 26379 axpasch 26410 axcontlem2 26434 axcontlem4 26436 axcontlem7 26439 axcontlem8 26440 neibastop3 33320 bj-0int 34011 ralbi12f 34989 iineq12f 34993 pmapglbx 36455 ordelordALTVD 40759 |
Copyright terms: Public domain | W3C validator |