Theorem r19.3rmv 3618

Description: Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.)

Assertion

Ref	Expression
r19.3rmv	⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜑(𝑦)

Proof of Theorem r19.3rmv

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 ⊢ Ⅎ𝑥𝜑
2	1	r19.3rm 3616	1 ⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wex 1545   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-ral 2533

This theorem is used by:  iinconstm  4021  exmidsssnc  4340  cnvpom  5330  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  ctssexmid  7491  exmidonfinlem  7546  caucvgsrlemasr  8158  resqrexlemgt0  11802  rmodislmodlem  14771  rmodislmod  14772  rabid1o  17200  stnot  17205  wexmiddiffilem  17209  wexmiddifxylem  17211