![]() |
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 1812. (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 214 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | |
2 | 1 | ral2imi 3074 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
3 | biimpr 219 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | |
4 | 3 | ral2imi 3074 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑)) |
5 | 2, 4 | impbid 211 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-ral 3051 |
This theorem is referenced by: rexbiOLD 3094 uniiunlem 4080 iineq2 5017 reusv2lem5 5402 ralrnmptw 7103 ralrnmpt 7105 f1mpt 7271 mpo2eqb 7553 ralrnmpo 7560 naddcom 8703 naddrid 8704 naddass 8717 rankonidlem 9858 acni2 10076 kmlem8 10187 kmlem13 10192 fimaxre3 12198 cau3lem 15342 rlim2 15481 rlim0 15493 rlim0lt 15494 catpropd 17697 funcres2b 17891 ulmss 26383 lgamgulmlem6 27016 colinearalg 28798 axpasch 28829 axcontlem2 28853 axcontlem4 28855 axcontlem7 28858 axcontlem8 28859 neibastop3 35979 bj-0int 36713 ralbi12f 37766 iineq12f 37770 pmapglbx 39374 ordelordALTVD 44450 |
Copyright terms: Public domain | W3C validator |