Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbidv2 | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.) |
Ref | Expression |
---|---|
ralbidv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
Ref | Expression |
---|---|
ralbidv2 | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbidv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) | |
2 | 1 | albidv 1836 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 2901 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 2901 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 302 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-ral 2901 |
This theorem is referenced by: ralbidva 2968 ralss 3631 oneqmini 5693 ordunisuc2 6936 dfsmo2 7331 wemapsolem 8338 zorn2lem1 9201 raluz 11612 limsupgle 14056 ello12 14095 elo12 14106 lo1resb 14143 rlimresb 14144 o1resb 14145 isprm3 15234 isprm7 15258 ist1 20935 ist1-2 20961 hausdiag 21258 xkopt 21268 cnflf 21616 cnfcf 21656 metcnp 22156 caucfil 22889 mdegleb 23628 eulerpartlemgvv 29765 filnetlem4 31546 hoidmvle 39490 elbigo2 42144 |
Copyright terms: Public domain | W3C validator |