Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssrexv | GIF version |
Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) |
Ref | Expression |
---|---|
ssrexv | ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3141 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 334 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | 2 | reximdv2 2569 | 1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ∃wrex 2449 ⊆ wss 3121 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-rex 2454 df-in 3127 df-ss 3134 |
This theorem is referenced by: iunss1 3882 moriotass 5834 tfr1onlemssrecs 6315 tfrcllemssrecs 6328 fiss 6950 supelti 6975 ctssdclemn0 7083 ctssdc 7086 enumctlemm 7087 lbzbi 9562 fiubm 10750 rexico 11172 alzdvds 11801 zsupcl 11889 infssuzex 11891 gcddvds 11905 dvdslegcd 11906 pclemub 12228 ssrest 12935 reeff1olem 13445 bj-charfunbi 13806 bj-nn0suc 13959 |
Copyright terms: Public domain | W3C validator |