Description: Obsolete version of rexss as of 14-Oct-2025. (Contributed by Stefan O'Rear, 3-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rexssOLD | ⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssel | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) | |
| 2 | 1 | pm4.71rd | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) ) |
| 3 | 2 | anbi1d | ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) ) ) |
| 4 | anass | ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) | |
| 5 | 3 4 | bitrdi | ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) ) |
| 6 | 5 | rexbidv2 | ⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) |