| 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 1818. (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 215 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | |
| 2 | 1 | ral2imi 3085 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
| 3 | biimpr 220 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | |
| 4 | 3 | ral2imi 3085 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑)) |
| 5 | 2, 4 | impbid 212 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: rexbiOLD 3105 uniiunlem 4087 iineq2 5012 reusv2lem5 5402 ralrnmptw 7114 ralrnmpt 7116 f1mpt 7281 mpo2eqb 7565 ralrnmpo 7572 naddcom 8720 naddrid 8721 naddass 8734 rankonidlem 9868 acni2 10086 kmlem8 10198 kmlem13 10203 fimaxre3 12214 cau3lem 15393 rlim2 15532 rlim0 15544 rlim0lt 15545 catpropd 17752 funcres2b 17942 ulmss 26440 lgamgulmlem6 27077 colinearalg 28925 axpasch 28956 axcontlem2 28980 axcontlem4 28982 axcontlem7 28985 axcontlem8 28986 neibastop3 36363 bj-0int 37102 ralbi12f 38167 iineq12f 38171 pmapglbx 39771 ordelordALTVD 44887 |
| Copyright terms: Public domain | W3C validator |