Metamath Proof Explorer

Theorem bj-eeanvw

Description: Version of exdistrv with a disjoint variable condition on x , y not requiring ax-11 . (The same can be done with eeeanv and ee4anv .) (Contributed by BJ, 29-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-eeanvw ⊢ ∃ x ∃ y φ ∧ ψ ↔ ∃ x φ ∧ ∃ y ψ

Proof

Step Hyp Ref Expression
1 19.42v ⊢ ∃ y φ ∧ ψ ↔ φ ∧ ∃ y ψ
2 1 exbii ⊢ ∃ x ∃ y φ ∧ ψ ↔ ∃ x φ ∧ ∃ y ψ
3 19.41v ⊢ ∃ x φ ∧ ∃ y ψ ↔ ∃ x φ ∧ ∃ y ψ
4 2 3 bitri ⊢ ∃ x ∃ y φ ∧ ψ ↔ ∃ x φ ∧ ∃ y ψ