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 1917 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 298 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ∈ wcel 2114 ∀wral 3138 |
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 3143 |
This theorem is referenced by: ralimdva 3177 ssralv 4021 zorn2lem7 9910 pwfseqlem3 10068 sup2 11583 xrsupexmnf 12685 xrinfmexpnf 12686 xrsupsslem 12687 xrinfmsslem 12688 xrub 12692 r19.29uz 14695 rexuzre 14697 caurcvg 15018 caucvg 15020 isprm5 16034 prmgaplem5 16374 prmgaplem6 16375 mrissmrid 16895 elcls3 21674 iscnp4 21854 cncls2 21864 cnntr 21866 2ndcsep 22050 dyadmbllem 24183 xrlimcnp 25532 pntlem3 26171 sigaclfu2 31387 lfuhgr2 32372 rdgssun 34675 mapdordlem2 38805 dffltz 39363 iunrelexp0 40137 climrec 41974 0ellimcdiv 42020 |
Copyright terms: Public domain | W3C validator |