Theorem 19.41v 963

Description: Special case of Theorem 19.41 of [Margaris] p. 90.

Assertion

Ref	Expression
19.41v	⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ))

Distinct variable group(s):   ψ,x

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (ψ → ∀xψ)
2	1	19.41 774	1 ⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ))

Syntax hints:   ↔ wb 127   ∧ wa 196  ∃wex 678

This theorem is referenced by:  19.41vv 964  19.41vvv 965  eeeanv 981  euanv 1053  r19.41v 1302  gencbvex 1372  euxfr 1436  sbcgf 1469  zfpair 1891  iunconst 2000  opabid 2099  opelxp 2452  dmuni 2538  dmres 2584  rnuni 2646  dminss 2648  imainss 2649  imaiun 2650  coass 2667  f11o 2821  rnoprab 3033  domen 3284  xpassen 3344  kmlem3 3582  cflem 3700  prnmadd 3894  genpass 3906  ltexprlem4 3939  reclem1pr 3950  reclem2pr 3951  suplem1pr 3955  elreal 4044

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679

metamath.org