![]() |
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 form). (Contributed by NM, 6-Apr-1997.) |
Ref | Expression |
---|---|
ralbidv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
Ref | Expression |
---|---|
ralbidv2 | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbidv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) | |
2 | 1 | albidv 1921 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3111 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3111 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 317 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1536 ∈ wcel 2111 ∀wral 3106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 |
This theorem depends on definitions: df-bi 210 df-ral 3111 |
This theorem is referenced by: ralbidva 3161 raleqbidv 3354 ralss 3985 oneqmini 6210 ordunisuc2 7539 dfsmo2 7967 wemapsolem 8998 zorn2lem1 9907 raluz 12284 limsupgle 14826 ello12 14865 elo12 14876 lo1resb 14913 rlimresb 14914 o1resb 14915 isprm3 16017 isprm7 16042 ist1-2 21952 hausdiag 22250 xkopt 22260 cnflf 22607 cnfcf 22647 metcnp 23148 caucfil 23887 mdegleb 24665 islinds5 30983 eulerpartlemgvv 31744 filnetlem4 33842 mnuunid 40985 hoidmvle 43239 elbigo2 44966 |
Copyright terms: Public domain | W3C validator |