Theorem r19.41v 3186

Description: Restricted quantifier version 19.41v 1946. Version of r19.41 3260 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.)

Assertion

Ref	Expression
r19.41v	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem r19.41v

Step	Hyp	Ref	Expression
1		df-rex 3068	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1844	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1946	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3068	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 224	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 627	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 299	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1775   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  r19.42v  3188  r19.41vv  3224  3reeanv  3227  reuxfr1d  3758  reuind  3761  iuncom4  5004  dfiun2gOLD  5035  iunxiun  5101  inuni  5355  xpiundi  5758  xpiundir  5759  imaco  6272  coiun  6277  abrexco  7263  imaiun  7264  isomin  7356  isoini  7357  imaeqsexvOLD  7382  imaeqexov  7670  oarec  8598  mapsnend  9074  unfi  9209  brttrcl2  9751  genpass  11046  4fvwrd4  13684  4sqlem12  16989  imasleval  17587  lsmspsn  21100  utoptop  24258  metrest  24552  metust  24586  cfilucfil  24587  metuel2  24593  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  addsdilem1  28191  0reno  28443  renegscl  28444  readdscl  28445  remulscl  28448  istrkg2ld  28482  axsegcon  28956  fusgreg2wsp  30364  nmoo0  30819  nmop0  32014  nmfn0  32015  rexunirn  32519  dmrab  32524  iunrnmptss  32585  ressupprn  32704  ordtconnlem1  33884  dya2icoseg2  34259  dya2iocnei  34263  omssubaddlem  34280  omssubadd  34281  satfvsuclem2  35344  satf0  35356  satffunlem1lem2  35387  satffunlem2lem2  35390  rexxfr3dALT  35623  bj-mpomptALT  37101  mptsnunlem  37320  fvineqsneq  37394  rabiun  37579  iundif1  37580  poimir  37639  ismblfin  37647  eldmqs1cossres  38640  erimeq2  38659  prter2  38862  prter3  38863  islshpat  38998  lshpsmreu  39090  islpln5  39517  islvol5  39561  cdlemftr3  40547  dvhb1dimN  40968  dib1dim  41147  mapdpglem3  41657  hdmapglem7a  41909  diophrex  42762  dfsclnbgr6  47781  r19.41dv  48650  reuxfr1dd  48654