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 1819. (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 217 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | |
2 | 1 | ral2imi 3158 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
3 | biimpr 222 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | |
4 | 3 | ral2imi 3158 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑)) |
5 | 2, 4 | impbid 214 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wral 3140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-ral 3145 |
This theorem is referenced by: uniiunlem 4063 iineq2 4941 reusv2lem5 5305 ralrnmptw 6862 ralrnmpt 6864 f1mpt 7021 mpo2eqb 7285 ralrnmpo 7291 rankonidlem 9259 acni2 9474 kmlem8 9585 kmlem13 9590 fimaxre3 11589 cau3lem 14716 rlim2 14855 rlim0 14867 rlim0lt 14868 catpropd 16981 funcres2b 17169 ulmss 24987 lgamgulmlem6 25613 colinearalg 26698 axpasch 26729 axcontlem2 26753 axcontlem4 26755 axcontlem7 26758 axcontlem8 26759 neibastop3 33712 bj-0int 34395 ralbi12f 35440 iineq12f 35444 pmapglbx 36907 ordelordALTVD 41208 |
Copyright terms: Public domain | W3C validator |