Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralimdv2 | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
Ref | Expression |
---|---|
ralimdv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) |
Ref | Expression |
---|---|
ralimdv2 | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) | |
2 | 1 | alimdv 1924 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3056 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3056 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 299 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1541 ∈ wcel 2112 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 |
This theorem depends on definitions: df-bi 210 df-ral 3056 |
This theorem is referenced by: ralimdva 3090 ssralv 3953 zorn2lem7 10081 pwfseqlem3 10239 sup2 11753 xrsupexmnf 12860 xrinfmexpnf 12861 xrsupsslem 12862 xrinfmsslem 12863 xrub 12867 r19.29uz 14879 rexuzre 14881 caurcvg 15205 caucvg 15207 isprm5 16227 prmgaplem5 16571 prmgaplem6 16572 mrissmrid 17098 elcls3 21934 iscnp4 22114 cncls2 22124 cnntr 22126 2ndcsep 22310 dyadmbllem 24450 xrlimcnp 25805 pntlem3 26444 sigaclfu2 31755 lfuhgr2 32747 rdgssun 35235 mapdordlem2 39337 sn-sup2 40088 dffltz 40115 iunrelexp0 40928 climrec 42762 0ellimcdiv 42808 |
Copyright terms: Public domain | W3C validator |