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 3145 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3145 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 316 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1535 ∈ wcel 2114 ∀wral 3140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-ral 3145 |
This theorem is referenced by: ralbidva 3198 raleqbidv 3403 ralss 4039 oneqmini 6244 ordunisuc2 7561 dfsmo2 7986 wemapsolem 9016 zorn2lem1 9920 raluz 12299 limsupgle 14836 ello12 14875 elo12 14886 lo1resb 14923 rlimresb 14924 o1resb 14925 isprm3 16029 isprm7 16054 ist1-2 21957 hausdiag 22255 xkopt 22265 cnflf 22612 cnfcf 22652 metcnp 23153 caucfil 23888 mdegleb 24660 islinds5 30934 eulerpartlemgvv 31636 filnetlem4 33731 mnuunid 40620 hoidmvle 42889 elbigo2 44619 |
Copyright terms: Public domain | W3C validator |