![]() |
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 1859. (Contributed by NM, 6-Oct-2003.) |
Ref | Expression |
---|---|
ralbi | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfra1 3043 | . 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) | |
2 | rspa 3032 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | ralbida 3084 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wral 3014 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-10 2132 ax-12 2160 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1818 df-nf 1823 df-ral 3019 |
This theorem is referenced by: uniiunlem 3798 iineq2 4646 reusv2lem5 4978 ralrnmpt 6483 f1mpt 6633 mpt22eqb 6886 ralrnmpt2 6892 rankonidlem 8804 acni2 8982 kmlem8 9092 kmlem13 9097 fimaxre3 11083 cau3lem 14214 rlim2 14347 rlim0 14359 rlim0lt 14360 catpropd 16491 funcres2b 16679 ulmss 24271 lgamgulmlem6 24880 colinearalg 25910 axpasch 25941 axcontlem2 25965 axcontlem4 25967 axcontlem7 25970 axcontlem8 25971 neibastop3 32584 bj-0int 33282 ralbi12f 34201 iineq12f 34205 pmapglbx 35475 ordelordALTVD 39519 |
Copyright terms: Public domain | W3C validator |